proposition: Lemma _paco_convert_rev2: forall T0 T1 (paco2: forall (y0: @T0) (y1: @T1 y0) , Prop) y0 y1 x0 x1 (EQ: _paco_id (@exist2T T0 T1 x0 x1 = @exist2T T0 T1 y0 y1)) (PACO: @paco2 y0 y1), @paco2 x0 x1.
proof: Proof. intros. apply (@f_equal (@sig2T T0 T1) _ (fun x => @paco2 x.(proj2T0) x.(proj2T1) )) in EQ. simpl in EQ. rewrite EQ. apply PACO. Qed.