module Goal2_OutOfOrder where
data Bool : Set where
true : Bool
false : Bool
data BoolOp : Set where
None : BoolOp
Some : Bool -> BoolOp
get : BoolOp -> Bool
get None = true
get (Some x) = x
postulate LHS : (B : Set) -> B -> Set
postulate RHS : (A : Set) -> (a : A) -> LHS A a
-- Atoms
postulate F : Bool -> Set
postulate P : (X : Set) -> (x : X) -> Set
mutual
alpha : Bool -> BoolOp
alpha x = _
-- Constraints
c1 : (P ((x : Bool) -> F (get (alpha x)) -> BoolOp) (\x -> \y -> None)) ->
(P ((_ : Bool) -> F true -> BoolOp) (\x -> \y -> alpha x))
c1 x = x