proposition: Lemma ap_phi0R : forall a, ap a ->{b : T1 | a = phi0 b}.
proof: Proof. destruct a. intro; elimtype False. inversion H. exists a1. inversion H. unfold phi0;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List