proposition: Lemma if_rule {A1 A2} {m1: M1 A1} {m2 : M2 A2} {w w'} (b:bool) : (if b then ⊨ m1 ≈ m2 [{ w }] else ⊨ m1 ≈ m2 [{ w' }]) -> ⊨ m1 ≈ m2 [{ if b then w else w' }].
proof: Proof. destruct b=> //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)