proposition: Lemma FILTER_def {_34398 : Type'} : (@FILTER _34398) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398) (fun FILTER' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_34398 -> Prop) -> (list _34398) -> list _34398 => forall _18185 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall P : _34398 -> Prop, (FILTER' _18185 P (@nil _34398)) = (@nil _34398)) /\ (forall h : _34398, forall P : _34398 -> Prop, forall t : list _34398, (FILTER' _18185 P (@cons _34398 h t)) = (@COND (list _34398) (P h) (@cons _34398 h (FILTER' _18185 P t)) (FILTER' _18185 P t)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))).
proof: Proof. exact (eq_refl (@FILTER _34398)). Qed.
imports: coq theory_hol types