proposition: Lemma positive_rect2_red2 : forall P c1 c2 c3 p, positive_rect2 P c1 c2 c3 (xO p) = c2 p (positive_rect2 P c1 c2 c3 p).
proof: Proof. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid