proposition: Theorem twoP_ind : forall P : list (Term A n) -> list (Term A n) -> Prop, (forall p q : list (Term A n), (forall r s : list (Term A n), lessP A n (r, s) (p, q) -> P r s) -> P p q) -> forall p q : list (Term A n), P p q.
proof: Proof. intros P H' p q; try assumption. change ((fun pq : list (Term A n) * list (Term A n) => P (ffst pq) (ssnd pq)) (p, q)) in |- *. cut (exists x : list (Term A n) * list (Term A n), x = ppair p q). unfold ppair in |- *; intros H'0; elim H'0; intros x E; rewrite <- E; clear H'0. pattern x in |- *; apply well_founded_ind with (A := (list (Term A n) * list (Term A n))%type) (R := lessP A n) (1 := wf_lessP A n); auto. intros x0 H'0; apply H'; auto. intros r s H'1. apply (H'0 (r, s)). generalize H'1; case x0; simpl in |- *; auto. exists (ppair p q); auto. Qed.