proposition: Lemma tFreshSubset : forall {G : CFGV} {vc : VarSym G} {sym : GSym G} (hlnew : list (vType vc)) (tsa tsb : list (Term sym)), tFresh hlnew tsa -> subset tsb tsa -> tFresh hlnew tsb.
proof: Proof. introns XX. unfold tFresh. unfold tFresh in XX. repnd; dands; [ SetReasoning | trivial]. Qed.
imports: Term AssociationList