proposition: Lemma HD_of_cons {A: Type'} (h: A) (t: list A) : @HD A (h :: t) = h.
proof: Proof. unfold HD. generalize (NUMERAL (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))); intro p. match goal with |- ε ?x _ _ = _=> set (Q := x) end. assert (i: exists q, Q q). exists (fun _=> @hd A (HD nil)). unfold Q. intro. simpl. trivial. generalize (ε_spec i). intro H. apply H. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List