proposition: Lemma unfold_process : forall x : ACProcess, x = match x with | ACTALK x x0 x1 x2 x3 => ((((ACTALK x) x0) x1) x2) x3 | ACLISTEN x x0 => (ACLISTEN x) x0 | ACPAR x x0 => (ACPAR x) x0 end.
proof: Proof. simple destruct x. trivial. trivial. trivial. Defined.