proposition: Lemma case_pure {A B C} (ac : A -> C) (bc : B -> C) : case_ (pure ac) (pure bc) ⩯ pure (@case_ _ Fun _ _ _ _ _ ac bc).
proof: Proof. intros []; reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.Monad Basics.CategoryFunctor Basics.CategoryKleisli Basics.Function)