proposition: Lemma ASSOC_def {_34421 _34427 : Type'} : (@ASSOC _34421 _34427) = (@ε ((prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421) (fun ASSOC' : (prod nat (prod nat (prod nat (prod nat nat)))) -> _34427 -> (list (prod _34427 _34421)) -> _34421 => forall _18192 : prod nat (prod nat (prod nat (prod nat nat))), forall h : prod _34427 _34421, forall a : _34427, forall t : list (prod _34427 _34421), (ASSOC' _18192 a (@cons (prod _34427 _34421) h t)) = (@COND _34421 ((@fst _34427 _34421 h) = a) (@snd _34427 _34421 h) (ASSOC' _18192 a t))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0))))))))))))).
proof: Proof. exact (eq_refl (@ASSOC _34421 _34427)). Qed.
imports: coq theory_hol types