proposition: Lemma nat_rect_rule {A1 A2} {m1: nat -> M1 A1} {m2 : nat -> M2 A2} {w0 wsuc} (w := nat_rect (fun=> dfst (W ⟨A1, A2⟩)) w0 wsuc) : ⊨ m1 0 ≈ m2 0 [{ w0 }] -> (forall n, ⊨ m1 n ≈ m2 n [{ w n }] -> ⊨ m1 (S n) ≈ m2 (S n) [{ wsuc n (w n) }]) -> forall n, ⊨ m1 n ≈ m2 n [{ w n }].
proof: Proof. induction n => //=. apply H0=> //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)