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