--#include "alfa/Prelude.alfa"

package Utils where
  open Logic  use  IsTrue
  open Module_Prelude
   use  Maybe,  maybe,  Bool,  PredTrue,  PredFalse,  (&&)
  MaybePropD (A::Set)
             (B::Set)
             (n::B)
             (j::A -> B)
             (m::Maybe A)
             (P::B -> Set)
             (pn::(===) (Maybe A) Nothing@_ m -> P n)
             (pj::(a::A) -> (===) (Maybe A) (Just@_ a) m -> P (j a))
    :: P (maybe B A n j m)
    = case m of {
        (Nothing) -> pn Ref@_;
        (Just a) -> pj a Ref@_;}
  IsPredTrue (b::Bool)(p::IsTrue b) :: PredTrue b
    = case b of {
        (False) -> p;
        (True) -> p;}
  PredIsTrue (b::Bool)(p::PredTrue b) :: IsTrue b
    = case b of {
        (False) -> p;
        (True) -> p;}
  BoolAndIntro (a::Bool)(b::Bool)(pa::PredTrue a)(pb::PredTrue b)
    :: PredTrue (a && b)
    = case a of {
        (False) -> case pa of { };
        (True) ->
          case b of {
            (False) -> case pb of { };
            (True) -> TrivialityIntro;};}
  BoolAndElim1 (a::Bool)(b::Bool)(p::PredTrue (a && b)) :: PredTrue a
    = case a of {
        (False) -> case p of { };
        (True) -> TrivialityIntro;}
  BoolAndElim2 (a::Bool)(b::Bool)(p::PredTrue (a && b)) :: PredTrue b
    = case a of {
        (False) ->
          case b of {
            (False) -> p;
            (True) -> TrivialityIntro;};
        (True) -> p;}
  excludedMiddle (b::Bool)(t::PredTrue b)(f::PredFalse b) :: Absurdity
    = case b of {
        (False) -> t;
        (True) -> f;}
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "MaybePropD" hide 6
var "BoolAndElim2" hide 2
var "BoolAndIntro" hide 2
var "excludedMiddle" hide 1
var "BoolAndElim1" hide 2
 #-}