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