proposition: Lemma AppR_Lambda' T s m: m = length T -> AppR (Lambda m s) T >* T .+ var • s.
proof: Proof. intros ?; replace (Lambda m s) with (var • Lambda m s) by now asimpl. replace m with (length T + 0) by lia. eapply AppR_Lambda with (n := 0). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)