module AutoProof where

open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality

data Bin : Set where O I : Bin

Bins : List Bin
Bins = (O ∷ I ∷ [])

xor2 : Bin → Bin → Bin
xor2 O O = O
xor2 O I = I
xor2 I O = I
xor2 I I = O

xor3 : Bin → Bin → Bin → Bin
xor3 x y z = xor2 x (xor2 y z)

infixr 30 _:all:_ 

data All {X : Set} (P : X -> Set) : List X -> Set where
  all[] : All P [] 
  _:all:_ : forall {x xs} -> P x -> All P xs -> All P (x ∷ xs)

AutoProof : (All (λ x → All (λ y → All (λ z → xor3 x y z ≡ xor3 z y x) Bins) Bins) Bins)
AutoProof = ((refl :all: refl :all: all[]) :all:
               (refl :all: refl :all: all[]) :all: all[])
              :all:
              ((refl :all: refl :all: all[]) :all:
               (refl :all: refl :all: all[]) :all: all[])
              :all: all[]