proposition: Lemma gensym_gt {A} {H : PreGensym A} (ls : list A) : forall x, List.In x ls -> (gensym ls > x)%gensym.
proof: Proof. intro x. induction ls as [|l ls IHls]; simpl. { intros []. } { intros [H'|H']; subst. { apply combine_respectful_l. } { etransitivity; [ apply combine_respectful_r | ]. apply IHls, H'. } } 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