Require Import List. Require Import LPTerm. Require Import WF. Require Import conversion. Require Import properties. Parameter OtherVars : Set. Axiom o_var_dec : forall (x y:OtherVars), {x = y} + {x <> y}. Axiom o_var_inf : forall (l : list OtherVars), exists x, ~ (In x l). Inductive Var := | Ctype | Cι| Co | Carrow | Cη | Cimpl | Cfa | Cε | V_a | V_b | V_c | V_x | V_y | V_z | V_F | V_G | V_X | V_Y | V_Z | V_f | V_g | V_other : OtherVars -> Var. Theorem var_dec : forall (x y:Var), {x = y} + {x <> y}. Proof. intros. induction x ; induction y; try (apply left; easy); try (apply right; easy). destruct (o_var_dec o o0). - left. rewrite e. easy. - right. intro. apply n. Qed. Axiom var_inf : forall l, exists x:Var, ~ (In x l). Parameter type : Var. Parameter ι : Var. Parameter o : Var. Parameter arrow : Var. Parameter η : Var. Parameter impl : Var. Parameter fa : Var. Parameter ε : Var. Parameter a b c x y z F G X Y Z f g : Var. Theorem util_var_decl c x A : c ✓ -> (c ✓ -> c, x : A ✓) -> c, x : A ✓. Proof. exact (fun x f => f x). Qed. Theorem util_rul_decl c t u : c ✓ -> (c ✓ -> c, t ≡ u ✓) -> c, t ≡ u ✓. Proof. exact (fun x f => f x). Qed. Definition STT := [] , type : TType , ι : # type , o : # type , arrow : # type ~> # type ~> # type , η : # type ~> TType , ε : # η @ # o ~> # η @ # o , impl : # η @ # o ~> # η @ # o ~> # η @ # o , fa : a ; # type ~> (# η @ # a ~> # η @ # o) ~> (# η @ # o) , x ; # type => y ; # type => # η @ (# arrow @ # x @ # y) ≡ x ; # type => y ; # type => (# η @ # x ~> # η @ # y) , x ; # type => y ; # type => # ε @ (# impl @ # x @ # y) ≡ x ; # type => y ; # type => (# ε @ # x ~> #ε @ # y) , a ; # type => f ; # type => # ε @ (#fa @ #a @ #f) ≡ a ; # type => f ; # type => z ; (#η @ #a) => # ε @ (#f @ #x) . Theorem STT_WF : STT ✓. Proof. try repeat apply util_rul_decl || apply util_var_decl. constructor. - intro. apply WFVarK. intro. inversion H0. inversion H1. constructor. constructor. - intro. constructor. intro. inversion H0. inversion H1. subst. apply TyAxiom. easy. repeat constructor. - intro. constructor. apply TyAxiom. easy. repeat constructor. - intro. constructor. apply TyPi. constructor. + easy. + repeat constructor. + intros. apply TyPi. * constructor. apply util_var_decl. -- easy. -- intro. apply WFVarT. apply TyAxiom. easy. repeat constructor. -- repeat constructor. * intros. apply TyAxiom. apply util_var_decl. apply util_var_decl. easy. intros. constructor. apply TyAxiom. easy. repeat constructor. intros. constructor. apply TyAxiom. easy. repeat constructor. repeat constructor. - intro. apply WFVarK. constructor. + constructor. easy. repeat constructor. + intros. constructor. constructor. constructor. easy. repeat constructor. - intros. apply WFVarT. constructor. + apply Qed.