7
data _≡_ {A : Set} (x : A) : A → Set where
10
foo : Bool → Bool → Bool
15
good : foo false true ≡ true
25
t₃ : Nat → Nat → Nat → T
27
bar : Nat → Nat → Nat → T
29
bar x y (suc z) = t₃ x y z
30
bar x (suc y) zero = t₂ x y
35
eqn₁ : bar a zero c ≡ t₂ a c
38
eqn₂ : bar a (suc b) (suc c) ≡ t₃ a (suc b) c
41
eqn₃ : bar a (suc b) zero ≡ t₂ a b