Library hydras.Ackermann.extEqualNat

From Coq Require Import Arith.


Fixpoint naryFunc (n : nat) : Set :=
  match n with
  | O ⇒ nat
  | S n ⇒ nat → naryFunc n
  end.


Fixpoint naryRel (n : nat) : Set :=
  match n with
  | O ⇒ bool
  | S n ⇒ nat → naryRel n
  end.


Fixpoint extEqual (n : nat) : ∀ (a b : naryFunc n), Prop :=
  match n with
    0 ⇒ fun a b ⇒ a = b
  | S p ⇒ fun a b ⇒ ∀ c, extEqual p (a c) (b c)
  end.


Fixpoint charFunction (n : nat) : naryRel n → naryFunc n :=
  match n return (naryRel n → naryFunc n) with
  | O ⇒ fun R : bool ⇒ match R with
                         | true ⇒ 1
                         | false ⇒ 0
                         end
  | S m ⇒ fun (R : naryRel (S m)) (a : nat) ⇒ charFunction m (R a)
  end.

Lemma extEqualRefl n a: extEqual n a a.

Lemma extEqualSym :
  ∀ (n : nat) (a b : naryFunc n), extEqual n a b → extEqual n b a.

Lemma extEqualTrans :
 ∀ (n : nat) (a b c : naryFunc n),
 extEqual n a b → extEqual n b c → extEqual n a c.