Commit 459012fa authored by Gaspard Ferey's avatar Gaspard Ferey

Finished proof.

parent a0fb638b
......@@ -193,15 +193,48 @@ Proof.
+exact (IHΓ H7 H10).
Qed.
Check (RSTClosure_ind RW_Beta_Gamma).
Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A t →β u -> Γ t →β u.
Proof.
intros.
induction H; econstructor.
Qed.
Lemma context_var_conv_Γ2 : forall Γ x A t u, Γ, x : A t →Γ u -> Γ t →Γ u.
Proof.
intros.
remember (Γ, x : A) as Γ0.
induction H.
destruct H ; inversion HeqΓ0.
- subst. econstructor. easy.
Qed.
Lemma context_var_conv_β : forall Γ x A t u, Γ, x : A t ↪β u -> Γ t ↪β u.
Proof.
Admitted.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. induction H. econstructor.
- apply CCApp1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_β2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_β2 Γ x A). easy.
Qed.
Lemma context_var_conv_Γ : forall Γ x A t u, Γ, x : A t ↪Γ u -> Γ t ↪Γ u.
Proof.
Admitted.
intros.
remember (Γ, x : A) as Γ0.
induction H; rewrite HeqΓ0 in H.
- econstructor. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCApp2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCAbs2. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi1. apply (context_var_conv_Γ2 Γ x A). easy.
- apply CCPi2. apply (context_var_conv_Γ2 Γ x A). easy.
Qed.
Lemma context_var_conv_βΓ : forall Γ x A t u, Γ, x : A t ↪βΓ u -> Γ t ↪βΓ u.
Proof.
......@@ -233,12 +266,12 @@ Proof.
- inversion H0 ; subst ; inversion H ; subst ; eapply IHΓ ; eassumption.
Qed.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ ; kind t -> False.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind t -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ ; t kind -> False.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ, t kind -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
......
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