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

fuck

parent ccb3ba8f
......@@ -137,6 +137,16 @@ Proof.
- now apply CVCtx.
Qed.
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
Proof.
induction Γ ; intros.
- inversion H0.
- inversion H0 ; subst.
+ inversion H ; subst. inversion H3 ; subst. eapply no_type_kind ; eassumption.
+ inversion H ; subst ; eapply IHΓ ; eassumption.
- inversion H0 ; subst ; inversion H ; subst ; eapply IHΓ ; eassumption.
Qed.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ ; kind t -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
......@@ -177,6 +187,56 @@ Proof.
* eassumption.
Qed.
Inductive of_typed_kind : term -> Prop :=
| IKType : of_typed_kind type
| IKPiType : forall A B, of_typed_kind B -> of_typed_kind (Π A ~ B).
(*
Lemma exchange : forall Γ x A y B t C, Γ, x : A -> Γ, y : B -> Γ, x : A, y : B t : C -> Γ, y : B, x : A t : C.
Proof.
intros.
induction H1.
- constructor.
+ constructor.
Lemma weakening : forall Γ x A t B, Γ, x : A -> Γ t : B -> Γ, x : A t : B.
Proof.
intros.
induction H0.
- constructor.
+ easy.
+ now constructor.
- now constructor.
- econstructor.
apply IHtyping1.
apply H.
*)
Lemma pi_is_sort : forall Γ A B t, Γ -> Γ t : Π A ~ B -> exists s, Γ Π A ~ B : s.
Proof.
intros.
induction H0.
- exists type.
inversion H1 ; subst.
inversion H ; subst.
Lemma inhabit_kind : forall Γ t, Γ -> Γ t : kind -> of_typed_kind t.
Proof.
intros.
remember kind as x.
induction H0 ; subst.
- exfalso ; eapply not_var_kind_gamma ; eassumption.
- constructor.
- assert (Γ, x : A ).
constructor ; eassumption.
pose proof (IHtyping2 H0 eq_refl).
now constructor.
- inversion Heqx.
-
Lemma inverse_kind : forall Γ t, Γ -> forall u, Γ u t -> u = kind <-> t = kind.
Proof.
intros.
......@@ -222,3 +282,4 @@ Proof.
pose proof (inverse_kind Γ B H3 kind H1).
now apply H2.
Qed.
*)
\ No newline at end of file
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