Commit a0fb638b authored by François Thiré's avatar François Thiré

add a missing piece of proof

parent e8936ab9
......@@ -220,7 +220,7 @@ Proof.
- econstructor.
- eapply CVSym ; now eapply IHRSTClosure.
- eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy.
-
- eapply CVRule ; eapply context_var_conv_βΓ ; now rewrite <- HeqΓ0.
Qed.
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment