proposition: Lemma _paco_convert_rev4: forall T0 T1 T2 T3 (paco4: forall (y0: @T0) (y1: @T1 y0) (y2: @T2 y0 y1) (y3: @T3 y0 y1 y2) , Prop) y0 y1 y2 y3 x0 x1 x2 x3 (EQ: _paco_id (@exist4T T0 T1 T2 T3 x0 x1 x2 x3 = @exist4T T0 T1 T2 T3 y0 y1 y2 y3)) (PACO: @paco4 y0 y1 y2 y3), @paco4 x0 x1 x2 x3.
proof: Proof. intros. apply (@f_equal (@sig4T T0 T1 T2 T3) _ (fun x => @paco4 x.(proj4T0) x.(proj4T1) x.(proj4T2) x.(proj4T3) )) in EQ. simpl in EQ. rewrite EQ. apply PACO. Qed.