proposition: Lemma MAP2_def {_34302 _34305 _34312 : Type'} : (@MAP2 _34302 _34305 _34312) = (@ε ((prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302) (fun MAP2' : (prod nat (prod nat (prod nat nat))) -> (_34305 -> _34312 -> _34302) -> (list _34305) -> (list _34312) -> list _34302 => forall _18174 : prod nat (prod nat (prod nat nat)), (forall f : _34305 -> _34312 -> _34302, forall l : list _34312, (MAP2' _18174 f (@nil _34305) l) = (@nil _34302)) /\ (forall h1' : _34305, forall f : _34305 -> _34312 -> _34302, forall t1 : list _34305, forall l : list _34312, (MAP2' _18174 f (@cons _34305 h1' t1) l) = (@cons _34302 (f h1' (@hd _34312 l)) (MAP2' _18174 f t1 (@tl _34312 l))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT1 0))))))))))).
proof: Proof. exact (eq_refl (@MAP2 _34302 _34305 _34312)). Qed.
imports: coq theory_hol types