Commit 841cc4d3 authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 73d1039d
......@@ -50,7 +50,7 @@ Proof. exact (fun x f => f x). Qed.
Definition STT := []
, type : TType
, type : TType
, ι : # type
, o : # type
, arrow : # type ~> # type ~> # type
......
......@@ -257,8 +257,9 @@ Qed.
Lemma weak_typable : forall Σ x A t, (Σ, x : A) WF -> typable Σ t -> typable (Σ, x : A) t.
Proof.
intros.
Admitted.
intros. destruct H0. destruct H0. eexists. eexists.
eapply weak_typ. apply H0. econstructor. inversion H; easy. easy.
Qed.
Lemma vardecl_typable2 : forall Σ x A, Σ WF -> x : A Σ -> typable Σ A.
Proof.
......@@ -326,12 +327,32 @@ Qed.
Definition inhabitable (Σ:signature) (T:term) : Prop := exists Γ t, Σ;Γ t : T.
Lemma abs_equiv : forall Σ Γ a A b B, Σ;Γ a : A -> Σ;(Γ,A) b : B -> Σ;Γ b[0 <- a] : B.
Proof.
intros.
generalize dependent H.
remember (Γ, A) as Γ'.
generalize dependent Γ.
induction H0; intros.
- simpl. econstructor. inversion HeqΓ'; subst.
eapply weak_checked.
Admitted.
Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u).
Proof.
intros. do 2 destruct H.
induction H.
- right. eapply vardecl_typable2. eapply weak_WF. apply H. apply H0.
-
- left. easy.
- exact IHtyping2.
- right. repeat eexists. econstructor. apply H. apply H0.
- right. destruct IHtyping1. inversion H1.
destruct H1. destruct H1. inversion H1; subst.
remember (Π A ~ B) as P.
inversion H; subst.
+
repeat eexists. apply H. apply H0
......
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