proposition: Lemma ALL2_def {_34213 _34220 : Type'} : (@ALL2 _34213 _34220) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop) (fun ALL2' : (prod nat (prod nat (prod nat nat))) -> (_34213 -> _34220 -> Prop) -> (list _34213) -> (list _34220) -> Prop => forall _18166 : prod nat (prod nat (prod nat nat)), (forall P : _34213 -> _34220 -> Prop, forall l2 : list _34220, (ALL2' _18166 P (@nil _34213) l2) = (l2 = (@nil _34220))) /\ (forall h1' : _34213, forall P : _34213 -> _34220 -> Prop, forall t1 : list _34213, forall l2 : list _34220, (ALL2' _18166 P (@cons _34213 h1' t1) l2) = (@COND Prop (l2 = (@nil _34220)) False ((P h1' (@hd _34220 l2)) /\ (ALL2' _18166 P t1 (@tl _34220 l2)))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))).
proof: Proof. exact (eq_refl (@ALL2 _34213 _34220)). Qed.
imports: coq theory_hol types