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