proposition: Lemma AppR_Lambda T s n sigma: AppR (sigma • Lambda (length T + n) s) T >* T .+ sigma • Lambda n s.
proof: Proof. revert s n sigma; induction T; intros; cbn [AppR length]; (eauto 2). replace (S (length T) + n) with (length T + S n) by lia. rewrite IHT; cbn; econstructor 2; (eauto 2); now asimpl. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)