proposition: Lemma ITLIST_def {_25350 _25351 : Type'} : (@fold_right_with_perm_args _25350 _25351) = (@ε ((prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350) (fun ITLIST' : (prod nat (prod nat (prod nat (prod nat (prod nat nat))))) -> (_25351 -> _25350 -> _25350) -> (list _25351) -> _25350 -> _25350 => forall _17988 : prod nat (prod nat (prod nat (prod nat (prod nat nat)))), (forall f : _25351 -> _25350 -> _25350, forall b : _25350, (ITLIST' _17988 f (@nil _25351) b) = b) /\ (forall h : _25351, forall f : _25351 -> _25350 -> _25350, forall t : list _25351, forall b : _25350, (ITLIST' _17988 f (@cons _25351 h t) b) = (f h (ITLIST' _17988 f t b)))) (@pair nat (prod nat (prod nat (prod nat (prod nat nat)))) (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat (prod nat (prod nat nat))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (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 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))))).
proof: Proof. generalize (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0))))))), (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT0 (BIT1 0))))))), (NUMERAL (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 0))))))), NUMERAL (BIT0 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))))))); intro p. apply fun_ext; intro f. apply fun_ext; intro l. apply fun_ext; intro a. match goal with |- _ = ε ?x _ _ _ _=> set (Q := x) end. assert (i: exists q, Q q). exists (fun _=> @fold_right_with_perm_args _25350 _25351). unfold Q. intro. simpl. auto. generalize (ε_spec i). intro H. symmetry. induction l; simpl. apply H. rewrite <- IHl. apply H. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List