proposition: Lemma pr1_pair : forall x y : E, pr1 (pair x y) = x.
proof: Proof. ir. set (u := pair x y) in *. assert (is_pair u). unfold u in |- *. ap pair_is_pair. pose(pair_recov H). unfold pair_recovers in (type of p). unfold u in (type of p). pose (lem1 p). am. Qed.
imports: tactics