proposition: Lemma FO_subst_equiv_eq Delta sigma Gamma (s t: exp X) A: (Delta ⊩(1) sigma : Gamma) -> (forall x, normal (sigma x)) -> normal s -> normal t -> (Gamma ⊢(1) s : A) -> (Gamma ⊢(1) t : A) -> sigma • s ≡ sigma • t -> sigma • s = sigma • t.
proof: Proof. intros. rewrite !subst_extensional with (sigma := sigma) (tau := fun x => if x el (vars s ++ vars t) then sigma x else var x). 2 - 3: intros; edestruct dec_in as [D|D]; simplify in D; intuition easy. eapply equiv_unique_normal_forms. easy. 1: rewrite !subst_extensional with (tau := sigma) (sigma := fun x => if x el (vars s ++ vars t) then sigma x else var x); eauto. 1 - 2: intros; edestruct dec_in as [D|D]; simplify in D; intuition easy. all: eapply normal_subst; eauto 2; intros x; destruct dec_in; eauto 2. all: simplify in i; destruct i as [V|V]; eapply vars_ordertyping in V as V'; eauto 2. all: destruct V' as (B & V1 & V2). all: eapply lambda_free_not_lam, lambda_free_subst; eauto 2. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)