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