test5
: ∀(x: Bool)
  (Equal Bool (Bool.not (Bool.not x)) x)
= λb
  (~b ?A ?T ?F)


//test5
//: (List Bool)
//= (List.cons ?A Bool.true
  //(List.cons ?B Bool.true
  //(List.cons ?C Bool.true
  //(List.nil ?D))))

// ?S : (?P true)  = (?P (F true))
// ?Z : (?P false) = (?P (F false))
// ?R : (?P b)     = (P (f b))

// ----------------------------------

//IsZero
//: ∀(n: Nat)
  //*
//= λn
  //∀(P: ∀(n: Nat) ∀(x: (IsZero n)) *)
  //∀(y: (P Nat.zero IsZero.y))
  //(P n self)

//F
//: ∀(n: Nat)
  //∀(e: IsZero (pred n)) 
  //(F n e)
//= (~e ?P ?B)


//?B : (?P Z        Yep)
//?R : (?P (pred n) e  ) = (F n e)




//?T : (?H True)
//?F : (?H False)
//RT : (?H x) = (Vector Nat (if x 1 else 0))


//Unif
//: ∀(b: Bool)
  //(Foo b)
//= λb (~b ?P Bool.true Bool.false)