proposition: Lemma envSubst_eq_trans : forall S1 S2 S3, S1 <=> S2 -> S2 <=> S3 -> S1 <=> S3.
proof: Proof. fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)