proposition: Lemma biinduction_iff `{Biinduction R} (P1 : Prop) (P2 : R → Prop) (P2_proper : Proper ((=) ==> iff) P2) : (P1 ↔ P2 0) → (∀ n, P2 n ↔ P2 (1 + n)) → ∀ n, P1 ↔ P2 n.
proof: Proof. intros ? ?. apply biinduction; [solve_proper | easy | firstorder]. Qed.
imports: Coq.Program.Program Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names