proposition: Lemma HD_def {A : Type'} : @hd A = @HD A.
proof: Proof. apply fun_ext. intro l. unfold hd, 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). unfold Q. intro. simpl. trivial. generalize (ε_spec i). intro H. destruct l; simpl. reflexivity. rewrite H. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List