-(*
-inductive redG : list T → list T → Prop ≝
- |redT : ∀A,B,G1,G2. red A B → redG G1 G2 →
- redG (A::G1) (B::G2)
- |redF : ∀A,G1,G2. redG G1 G2 → redG (A::G1) (A::G2).
-
-lemma redG_inv: ∀A,G,G1. redG (A::G) G1 →
- ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2.
-#A #G #G1 #rg (inversion rg)
- [#H destruct
- |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct
- #H1 @(ex_intro … B1) @(ex_intro … G3) % // % //
- ]
-qed. *)
-
-axiom conv_prod_split: ∀A,A1,B,B1. conv (Prod A B) (Prod A1 B1) →
-conv A A1 ∧ conv B B1.
+axiom conv_prod_split: ∀P,A,A1,B,B1.
+ Co P(Prod A B) (Prod A1 B1) → Co P A A1 ∧ Co P B B1.