proposition: Lemma EL_def {_34373 : Type'} : (@EL _34373) = (@ε ((prod nat nat) -> nat -> (list _34373) -> _34373) (fun EL' : (prod nat nat) -> nat -> (list _34373) -> _34373 => forall _18178 : prod nat nat, (forall l : list _34373, (EL' _18178 (NUMERAL 0) l) = (@hd _34373 l)) /\ (forall n : nat, forall l : list _34373, (EL' _18178 (S n) l) = (EL' _18178 n (@tl _34373 l)))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))))).
proof: Proof. exact (eq_refl (@EL _34373)). Qed.
imports: coq theory_hol types