extra assumptions in case zippers
Closed this issue · 0 comments
ivoysey commented
do we need the premises (Γ ,, (y , t2)) ⊢ e2 <= t and (Γ ,, (x , t1)) ⊢ e1 <= t ) in the AACaseZip rules? remove them and see.
Closed this issue · 0 comments
do we need the premises (Γ ,, (y , t2)) ⊢ e2 <= t and (Γ ,, (x , t1)) ⊢ e1 <= t ) in the AACaseZip rules? remove them and see.