proposition: Lemma ZIP_def {_34523 _34531 : Type'} : (@ZIP _34523 _34531) = (@ε ((prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531)) (fun ZIP' : (prod nat (prod nat nat)) -> (list _34523) -> (list _34531) -> list (prod _34523 _34531) => forall _18205 : prod nat (prod nat nat), (forall l2 : list _34531, (ZIP' _18205 (@nil _34523) l2) = (@nil (prod _34523 _34531))) /\ (forall h1' : _34523, forall t1 : list _34523, forall l2 : list _34531, (ZIP' _18205 (@cons _34523 h1' t1) l2) = (@cons (prod _34523 _34531) (@pair _34523 _34531 h1' (@hd _34531 l2)) (ZIP' _18205 t1 (@tl _34531 l2))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))))))).
proof: Proof. exact (eq_refl (@ZIP _34523 _34531)). Qed.
imports: coq theory_hol types