proposition: Lemma test_pick_fresh : forall (x y z : var) (L1 L2 L3 : vars) (t1 t2 : trm), True.
proof: Proof. Proof using. intros. pick_fresh a. Abort. End LibVarDemo. End LibVarDemos. From TLC Require Import LibSet. Lemma inter_union_disjoint_right: forall A (E F G : set A), F \# G -> (E \u F) \n G = (E \n G). Proof using. set_prove. Qed.
imports: TLC(LibTactics) TLC(LibLogic LibEqual LibList LibRelation LibWf LibList LibLN)