fact: Axiom thm_ITLIST : forall {_34154 _34155 : Type'} (h : _34155) (f : _34155 -> _34154 -> _34154) (t : list _34155) (b : _34154), ((@fold_right_with_perm_args _34154 _34155 f (@nil _34155) b) = b) /\ ((@fold_right_with_perm_args _34154 _34155 f (@cons _34155 h t) b) = (f h (@fold_right_with_perm_args _34154 _34155 f t b))).
imports: coq theory_hol types terms axioms