proposition: Lemma singletonSubst_cond M : isSingletonSubst M {x/M}.
proof: Proof. constructor; constructor. destruct i; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)