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