fact: Definition ifTE {A} {W} {D : Dijkstra W} {w1 w2 : W A} : forall (b: bool), D A w1 -> D A w2 -> D A (if b then w1 else w2) := fun b tt ff => match b as b return D A (if b then w1 else w2) with | true => tt | false => ff end.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)