proposition: Lemma subst_type M G (C: correct_subst M G) : type (subst C) = type M.
proof: Proof. unfold subst. destruct (subst_aux C); simpl; tauto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)