proposition: Lemma _paco_convert_rev1: forall T0 (paco1: forall (y0: @T0) , Prop) y0 x0 (EQ: _paco_id (@exist1T T0 x0 = @exist1T T0 y0)) (PACO: @paco1 y0), @paco1 x0.
proof: Proof. intros. apply (@f_equal (@sig1T T0) _ (fun x => @paco1 x.(proj1T0) )) in EQ. simpl in EQ. rewrite EQ. apply PACO. Qed.