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

where are we going to?

parent 846051ed
......@@ -193,14 +193,34 @@ Proof.
+exact (IHΓ H7 H10).
Qed.
Check (RSTClosure_ind RW_Beta_Gamma).
Lemma context_var_conv_β : forall Γ x A t u, Γ, x : A t ↪β u -> Γ t ↪β u.
Proof.
Admitted.
Lemma context_var_conv_Γ : forall Γ x A t u, Γ, x : A t ↪Γ u -> Γ t ↪Γ u.
Proof.
Admitted.
Lemma context_var_conv_βΓ : forall Γ x A t u, Γ, x : A t ↪βΓ u -> Γ t ↪βΓ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
destruct H.
- left ; eapply context_var_conv_β ; now rewrite <- HeqΓ0.
- right ; eapply context_var_conv_Γ ; now rewrite <- HeqΓ0.
Qed.
Lemma context_var_conv : forall Γ x A t u, Γ, x : A t u -> Γ t u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H.
- exact (CVRefl RW_Beta_Gamma Γ t).
- exact (CVSym RW_Beta_Gamma Γ t u IHRSTClosure).
- exact (CVTrans RW_Beta_Gamma Γ t u v IHRSTClosure1 IHRSTClosure2).
-
- econstructor.
- eapply CVSym ; now eapply IHRSTClosure.
- eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy.
-
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