proposition: Lemma fresh_union_l : forall xs L1 L2 n, fresh L1 n xs -> fresh L2 n xs -> fresh (L1 \u L2) n xs.
proof: Proof. Proof using. induction xs; simpl; intros; destruct n; tryfalse*. auto. destruct H. destruct H0. split~. forwards~ K: (@IHxs (L1 \u \{a}) (L2 \u \{a}) n). rewrite <- (union_same \{a}). rewrite union_assoc. rewrite <- (union_assoc L1). rewrite (union_comm L2). rewrite (union_assoc L1). rewrite* <- union_assoc. Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)