proposition: Lemma AppL_subst sigma S t: sigma • AppL S t = AppL (sigma •₊ S) (sigma • t).
proof: Proof. induction S; cbn; congruence. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)