proposition: Lemma ALLPAIRS_def {_34590 _34591 : Type'} : (@ALLPAIRS _34590 _34591) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop) (fun ALLPAIRS' : (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))))) -> (_34591 -> _34590 -> Prop) -> (list _34591) -> (list _34590) -> Prop => forall _18213 : prod nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))), (forall f : _34591 -> _34590 -> Prop, forall l : list _34590, (ALLPAIRS' _18213 f (@nil _34591) l) = True) /\ (forall h : _34591, forall f : _34591 -> _34590 -> Prop, forall t : list _34591, forall l : list _34590, (ALLPAIRS' _18213 f (@cons _34591 h t) l) = ((@List.Forall _34590 (f h) l) /\ (ALLPAIRS' _18213 f t l)))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat (prod nat nat)))))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))))).
proof: Proof. exact (eq_refl (@ALLPAIRS _34590 _34591)). Qed.
imports: coq theory_hol types