proposition: Lemma _paco_convert_rev5: forall T0 T1 T2 T3 T4 (paco5: forall (y0: @T0) (y1: @T1 y0) (y2: @T2 y0 y1) (y3: @T3 y0 y1 y2) (y4: @T4 y0 y1 y2 y3) , Prop) y0 y1 y2 y3 y4 x0 x1 x2 x3 x4 (EQ: _paco_id (@exist5T T0 T1 T2 T3 T4 x0 x1 x2 x3 x4 = @exist5T T0 T1 T2 T3 T4 y0 y1 y2 y3 y4)) (PACO: @paco5 y0 y1 y2 y3 y4), @paco5 x0 x1 x2 x3 x4.
proof: Proof. intros. apply (@f_equal (@sig5T T0 T1 T2 T3 T4) _ (fun x => @paco5 x.(proj5T0) x.(proj5T1) x.(proj5T2) x.(proj5T3) x.(proj5T4) )) in EQ. simpl in EQ. rewrite EQ. apply PACO. Qed.