proposition: Lemma MakeAbsPnodeSame : forall {G : CFGV} {vc : VarSym G} (lps : list (GSym G)) (m: Mixture (map (fun x : GSym G => (true, x)) (lps))), (MakeAbstractionsPNode vc m) = (MakeAbstractionsTNodeAux vc [] m).
proof: Proof. induction m; cpx. Qed.
imports: AlphaEquality SwapProps