proposition: Lemma tFresh_app : forall g l (l1 l2 : list (Term g)), @tFresh G vc g l (l1 ++ l2) <=> (tFresh l l1 # tFresh l l2).
proof: Proof. introv. unfold tFresh. rw flat_map_app. rw disjoint_app_r. split; sp. Qed.
imports: AlphaEquality SwapProps Eqdep_dec