proposition: Lemma AppR_vars s T: vars (AppR s T) === vars s ++ Vars T.
proof: Proof. induction T; cbn; simplify; lauto. rewrite IHT, <-app_assoc; eapply proper_app_seteq; lauto. eauto using app_comm. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)