proposition: Lemma option_eq {A : Type'} : @option_pred A = @option_ind A.
proof: Proof. apply fun_ext; intro r. apply prop_ext. intro h. apply h. intros r' [i|[a'' i]]; subst. apply option_ind0. apply option_ind1. induction 1; unfold option_pred; intros r h; apply h. left. reflexivity. right. exists a''. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance