proposition: Lemma _paco_convert1: forall T0 (paco1: forall (y0: @T0) , Prop) y0 (CONVERT: forall (x0: @T0) (EQ: _paco_id (@exist1T T0 x0 = @exist1T T0 y0)) , @paco1 x0), @paco1 y0.
proof: Proof. intros. apply CONVERT; reflexivity. Qed.