Commit 6d2a5c7d authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 68be8091
......@@ -123,8 +123,7 @@ Theorem right_arr_type : forall Γ t u AB, Γ ⊢ t ~> u : AB ->
Proof.
Admitted.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> v Γ.
Proof.
intros Γ t ; revert Γ ; induction t; intros ; try inversion H0.
- subst. induction H.
......
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