proposition: Lemma gensym_fresh {A} {H : PreGensym A} (ls : list A) : ~List.In (gensym ls) ls.
proof: Proof. intro H'. apply gensym_gt in H'. apply asymmetry in H'; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Lists.List Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Fiat.Common.StringFacts