proposition: Theorem PWO_Seq_P2_wf : forall x y, well_formed_comp (PWO_Seq_P2 x y).
proof: Proof. intuition. unfold PWO_Seq_P2. destruct (snd x); destruct (fst x); wftac. eapply P3_wf. eapply P1_wf. eapply P2_wf. eapply P2_wf. eapply P2_wf. Qed.
imports: FCF CompFold