proposition: Lemma sub_eq_id s t : (forall x, In x (vars t) -> s x = Var x) -> sub s t = t.
proof: Proof. intro. trans (sub id t). apply sub_eq. hyp. apply sub_id. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)