Prove the fundamental theorem

theories/soundness.v

@@ -0,0 +1,11 @@
+Require Import Autosubst2.fintype Autosubst2.syntax.
+Require Import fp_red logrel typing.
+From Hammer Require Import Tactics.
+
+Theorem fundamental_theorem :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A).
+  apply wt_mutual; eauto with sem;[idtac].
+  hauto l:on use:SE_Pair.
+Qed.

theories/typing.v

@@ -114,3 +114,9 @@ with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
 
 where
 "Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A).
+
+Scheme wf_ind := Induction for Wff Sort Prop
+  with wt_ind := Induction for Wt Sort Prop
+  with eq_ind := Induction for Eq Sort Prop.
+
+Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind.