proposition: Lemma _paco_convert2: forall T0 T1 (paco2: forall (y0: @T0) (y1: @T1 y0) , Prop) y0 y1 (CONVERT: forall (x0: @T0) (x1: @T1 x0) (EQ: _paco_id (@exist2T T0 T1 x0 x1 = @exist2T T0 T1 y0 y1)) , @paco2 x0 x1), @paco2 y0 y1.
proof: Proof. intros. apply CONVERT; reflexivity. Qed.