tt('const/fmapal/AP_SND', ty, ![A : $t, B : $t, C : $t]: ((B > C) > (('type/pair/prod' A B) > ('type/pair/prod' A C)))).
tt('const/fmapal/FMAPAL', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/finite_map/fmap' A B)))).
tt('const/fmapal/OFU', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A B))))).
tt('const/fmapal/OPTION_FLAT', ty, ![Z : $t]: (('type/list/list' ('type/option/option' ('type/list/list' Z))) > ('type/list/list' Z))).
tt('const/fmapal/OPTION_UPDATE', ty, ![A : $t, B : $t]: ((A > ('type/option/option' B)) > ((A > ('type/option/option' B)) > (A > ('type/option/option' B))))).
tt('const/fmapal/ORL', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > $o))).
tt('const/fmapal/ORL_bt', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o))).
tt('const/fmapal/ORL_bt_lb', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o)))).
tt('const/fmapal/ORL_bt_lb_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o)).
tt('const/fmapal/ORL_bt_lb_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o))))).
tt('const/fmapal/ORL_bt_lb_ub_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o)).
tt('const/fmapal/ORL_bt_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o)).
tt('const/fmapal/ORL_bt_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o)))).
tt('const/fmapal/ORL_bt_ub_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o)).
tt('const/fmapal/ORL_sublists', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > $o))).
tt('const/fmapal/ORL_sublists_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > $o)).
tt('const/fmapal/ORL_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > $o)).
tt('const/fmapal/ORWL', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/finite_map/fmap' A B) > (('type/list/list' ('type/pair/prod' A B)) > $o)))).
tt('const/fmapal/UFO', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A B))))).
tt('const/fmapal/assocv', ty, ![A : $t, B : $t]: (('type/list/list' ('type/pair/prod' A B)) > (A > ('type/option/option' B)))).
tt('const/fmapal/assocv_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > ('type/option/option' B))).
tt('const/fmapal/bl_to_fmap', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bl' ('type/pair/prod' A B)) > ('type/finite_map/fmap' A B)))).
tt('const/fmapal/bl_to_fmap_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > ('type/finite_map/fmap' A B))).
tt('const/fmapal/bt_map', ty, ![A : $t, B : $t]: ((A > B) > (('type/enumeral/bt' A) > ('type/enumeral/bt' B)))).
tt('const/fmapal/bt_rplacv_cn', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/pair/prod' A B) > (('type/enumeral/bt' ('type/pair/prod' A B)) > ((('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))) > ('type/enumeral/bt' ('type/pair/prod' A B))))))).
tt('const/fmapal/bt_rplacv_cn_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > ('type/enumeral/bt' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_fmap_lb', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/finite_map/fmap' A B))))).
tt('const/fmapal/bt_to_fmap_lb_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > ('type/finite_map/fmap' A B)))))).
tt('const/fmapal/bt_to_fmap_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > ('type/finite_map/fmap' A B))).
tt('const/fmapal/bt_to_fmap_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > ('type/finite_map/fmap' A B))))).
tt('const/fmapal/bt_to_orl', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))).
tt('const/fmapal/bt_to_orl_ac', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/bt_to_orl_ac_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_lb', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/bt_to_orl_lb_ac', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))))).
tt('const/fmapal/bt_to_orl_lb_ac_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_lb_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_lb_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > ('type/list/list' ('type/pair/prod' A B))))))).
tt('const/fmapal/bt_to_orl_lb_ub_ac', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))))).
tt('const/fmapal/bt_to_orl_lb_ub_ac_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_lb_ub_ac_tupled_aux', ty, ![A : $t, B : $t]: ((('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > $o)) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/pair/prod' A B))))).
tt('const/fmapal/bt_to_orl_lb_ub_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_ub', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/bt_to_orl_ub_ac', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))))).
tt('const/fmapal/bt_to_orl_ub_ac_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/bt_to_orl_ub_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/diff_merge', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' A) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/diff_merge_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/fmap', ty, ![A : $t, B : $t]: (('type/list/list' ('type/pair/prod' A B)) > ('type/finite_map/fmap' A B))).
tt('const/fmapal/incr_build', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))).
tt('const/fmapal/incr_flat', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B))))).
tt('const/fmapal/incr_merge', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))))).
tt('const/fmapal/incr_merge_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/incr_sort', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))).
tt('const/fmapal/inter_merge', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' A) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/inter_merge_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/list_rplacv_cn', ty, ![A : $t, B : $t]: (('type/pair/prod' A B) > (('type/list/list' ('type/pair/prod' A B)) > ((('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/list_rplacv_cn_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/merge', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/merge_out', ty, ![A : $t, B : $t]: (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B)))))).
tt('const/fmapal/merge_out_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/merge_tupled', ty, ![A : $t, B : $t]: (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B)))).
tt('const/fmapal/optry', ty, ![Z : $t]: (('type/option/option' Z) > (('type/option/option' Z) > ('type/option/option' Z)))).
tt('const/fmapal/optry_list', ty, ![G : $t, Z : $t]: ((Z > ('type/option/option' G)) > (('type/list/list' ('type/option/option' Z)) > ('type/option/option' G)))).
tt('const/fmapal/optry_list_tupled', ty, ![G : $t, Z : $t]: (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > ('type/option/option' G))).
tt('const/fmapal/unlookup', ty, ![A : $t, B : $t]: ((A > ('type/option/option' B)) > ('type/finite_map/fmap' A B))).
tt('const/fmapal/vcossa', ty, ![A : $t, B : $t]: (A > (('type/list/list' ('type/pair/prod' A B)) > ('type/option/option' B)))).
tt('thm/fmapal/ORL_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B)))) R) & (![b : B, a : A, l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) cmp l) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l))))))) (^[ORL_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) > $o), 'a\'' : ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) 'a\'' (^[cmp : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B))]: (('const/list/list_CASE' ('type/pair/prod' A B) $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' $o A B) v2 (^[a : A, b : B]: (('const/combin/I' $o) ((ORL_tupled (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) cmp l)) & (![p : A, q : B]: ((('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) p q) (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) l)) => ((('const/toto/apto' A) cmp a p) = 'const/toto/LESS'))))))))))))))).
tt('thm/fmapal/ORL_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) x x1) = (('const/fmapal/ORL_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/pair/prod' A B))) x x1))))).
tt('thm/fmapal/ORL_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), a : A, b : B, l : ('type/list/list' ('type/pair/prod' A B))]: ((P cmp l) => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1))))).
tt('thm/fmapal/ORL_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL' A B) cmp ('const/list/NIL' ('type/pair/prod' A B))) = $true))).
tt('thm/fmapal/ORL_e1', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : B, a : A]: ((('const/fmapal/ORL' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l)) = ((('const/fmapal/ORL' A B) cmp l) & (![p : A, q : B]: ((('const/bool/IN' ('type/pair/prod' A B)) (('const/pair/,' A B) p q) (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) l)) => ((('const/toto/apto' A) cmp a p) = 'const/toto/LESS'))))))).
tt('thm/fmapal/optry_0', def, ![Z : $t]: (![p : Z, q : ('type/option/option' Z)]: ((('const/fmapal/optry' Z) (('const/option/SOME' Z) p) q) = (('const/option/SOME' Z) p)))).
tt('thm/fmapal/optry_e1', def, ![Z : $t]: (![q : ('type/option/option' Z)]: ((('const/fmapal/optry' Z) ('const/option/NONE' Z) q) = q))).
tt('thm/fmapal/optry_list_tupled_primitive_', def, ![Z : $t, G : $t]: (('const/fmapal/optry_list_tupled' G Z) = (('const/relation/WFREC' ('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) ('type/option/option' G)) (('const/min/@' (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > $o))) (^[R : (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > $o))]: ((('const/relation/WF' ('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z)))) R) & ((![l : ('type/list/list' ('type/option/option' Z)), f : (Z > ('type/option/option' G))]: (R (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f l) (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f (('const/list/CONS' ('type/option/option' Z)) ('const/option/NONE' Z) l)))) & (![z : Z, l : ('type/list/list' ('type/option/option' Z)), f : (Z > ('type/option/option' G))]: (R (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f l) (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f (('const/list/CONS' ('type/option/option' Z)) (('const/option/SOME' Z) z) l)))))))) (^[optry_list_tupled : (('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) > ('type/option/option' G)), a : ('type/pair/prod' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z)))]: (('const/pair/pair_CASE' ('type/option/option' G) (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) a (^[f : (Z > ('type/option/option' G)), v1 : ('type/list/list' ('type/option/option' Z))]: (('const/list/list_CASE' ('type/option/option' Z) ('type/option/option' G)) v1 (('const/combin/I' ('type/option/option' G)) ('const/option/NONE' G)) (^[v2 : ('type/option/option' Z), l : ('type/list/list' ('type/option/option' Z))]: (('const/option/option_CASE' Z ('type/option/option' G)) v2 (('const/combin/I' ('type/option/option' G)) (optry_list_tupled (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f l))) (^[z : Z]: (('const/combin/I' ('type/option/option' G)) (('const/fmapal/optry' G) (f z) (optry_list_tupled (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) f l)))))))))))))).
tt('thm/fmapal/optry_list_curried_', def, ![Z : $t, G : $t]: (![x : (Z > ('type/option/option' G)), x1 : ('type/list/list' ('type/option/option' Z))]: ((('const/fmapal/optry_list' G Z) x x1) = (('const/fmapal/optry_list_tupled' G Z) (('const/pair/,' (Z > ('type/option/option' G)) ('type/list/list' ('type/option/option' Z))) x x1))))).
tt('thm/fmapal/optry_list_ind_', ax, ![Z : $t, G : $t]: (![P : ((Z > ('type/option/option' G)) > (('type/list/list' ('type/option/option' Z)) > $o))]: (((![f : (Z > ('type/option/option' G))]: (P f ('const/list/NIL' ('type/option/option' Z)))) & ((![f : (Z > ('type/option/option' G)), l : ('type/list/list' ('type/option/option' Z))]: ((P f l) => (P f (('const/list/CONS' ('type/option/option' Z)) ('const/option/NONE' Z) l)))) & (![f : (Z > ('type/option/option' G)), z : Z, l : ('type/list/list' ('type/option/option' Z))]: ((P f l) => (P f (('const/list/CONS' ('type/option/option' Z)) (('const/option/SOME' Z) z) l)))))) => (![v : (Z > ('type/option/option' G)), v1 : ('type/list/list' ('type/option/option' Z))]: (P v v1))))).
tt('thm/fmapal/optry_list_0', ax, ![G : $t, Z : $t]: (![f : (Z > ('type/option/option' G))]: ((('const/fmapal/optry_list' G Z) f ('const/list/NIL' ('type/option/option' Z))) = ('const/option/NONE' G)))).
tt('thm/fmapal/optry_list_1', ax, ![Z : $t, G : $t]: (![l : ('type/list/list' ('type/option/option' Z)), f : (Z > ('type/option/option' G))]: ((('const/fmapal/optry_list' G Z) f (('const/list/CONS' ('type/option/option' Z)) ('const/option/NONE' Z) l)) = (('const/fmapal/optry_list' G Z) f l)))).
tt('thm/fmapal/optry_list_e2', ax, ![Z : $t, G : $t]: (![z : Z, l : ('type/list/list' ('type/option/option' Z)), f : (Z > ('type/option/option' G))]: ((('const/fmapal/optry_list' G Z) f (('const/list/CONS' ('type/option/option' Z)) (('const/option/SOME' Z) z) l)) = (('const/fmapal/optry' G) (f z) (('const/fmapal/optry_list' G Z) f l))))).
tt('thm/fmapal/assocv_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/assocv_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) ('type/option/option' B)) (('const/min/@' (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > $o))) (^[R : (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A)) R) & (![y : B, l : ('type/list/list' ('type/pair/prod' A B)), x : A, a : A]: ((~ (a = x)) => (R (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) A) l a) (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) A) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) l) a))))))) (^[assocv_tupled : (('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A) > ('type/option/option' B)), 'a\'' : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) A)]: (('const/pair/pair_CASE' ('type/option/option' B) ('type/list/list' ('type/pair/prod' A B)) A) 'a\'' (^[v : ('type/list/list' ('type/pair/prod' A B)), a : A]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/option/option' B)) v (('const/combin/I' ('type/option/option' B)) ('const/option/NONE' B)) (^[v2 : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/option/option' B) A B) v2 (^[x : A, y : B]: (('const/combin/I' ('type/option/option' B)) (('const/bool/COND' ('type/option/option' B)) (a = x) (('const/option/SOME' B) y) (assocv_tupled (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) A) l a)))))))))))))).
tt('thm/fmapal/assocv_curried_', def, ![A : $t, B : $t]: (![x : ('type/list/list' ('type/pair/prod' A B)), x1 : A]: ((('const/fmapal/assocv' A B) x x1) = (('const/fmapal/assocv_tupled' A B) (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) A) x x1))))).
tt('thm/fmapal/assocv_ind_', ax, ![A : $t, B : $t]: (![P : (('type/list/list' ('type/pair/prod' A B)) > (A > $o))]: (((![a : A]: (P ('const/list/NIL' ('type/pair/prod' A B)) a)) & (![x : A, y : B, l : ('type/list/list' ('type/pair/prod' A B)), a : A]: (((~ (a = x)) => (P l a)) => (P (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) l) a)))) => (![v : ('type/list/list' ('type/pair/prod' A B)), v1 : A]: (P v v1))))).
tt('thm/fmapal/assocv_0', ax, ![B : $t, A : $t]: (![a : A]: ((('const/fmapal/assocv' A B) ('const/list/NIL' ('type/pair/prod' A B)) a) = ('const/option/NONE' B)))).
tt('thm/fmapal/assocv_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, l : ('type/list/list' ('type/pair/prod' A B)), a : A]: ((('const/fmapal/assocv' A B) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) l) a) = (('const/bool/COND' ('type/option/option' B)) (a = x) (('const/option/SOME' B) y) (('const/fmapal/assocv' A B) l a))))).
tt('thm/fmapal/vcossa_', def, ![A : $t, B : $t]: (![a : A, l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/vcossa' A B) a l) = (('const/fmapal/assocv' A B) l a)))).
tt('thm/fmapal/OPTION_UPDATE_', def, ![A : $t, B : $t]: (![f : (A > ('type/option/option' B)), g : (A > ('type/option/option' B)), x : A]: ((('const/fmapal/OPTION_UPDATE' A B) f g x) = (('const/fmapal/optry' B) (f x) (g x))))).
tt('thm/fmapal/merge_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/merge_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) R) & ((![b2 : B, b1 : B, l2 : ('type/list/list' ('type/pair/prod' A B)), l1 : ('type/list/list' ('type/pair/prod' A B)), a2 : A, a1 : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a1 a2) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) l1 l2)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2)))))) & ((![b2 : B, l2 : ('type/list/list' ('type/pair/prod' A B)), l1 : ('type/list/list' ('type/pair/prod' A B)), b1 : B, a2 : A, a1 : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a1 a2) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) l2)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2)))))) & (![b1 : B, l2 : ('type/list/list' ('type/pair/prod' A B)), b2 : B, l1 : ('type/list/list' ('type/pair/prod' A B)), a2 : A, a1 : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a1 a2) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) l1 (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2))))))))))) (^[merge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) v1 (^[v2 : ('type/list/list' ('type/pair/prod' A B)), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) l) (^[v6 : ('type/pair/prod' A B), l1 : ('type/list/list' ('type/pair/prod' A B))]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) l (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) v6 l1)) (^[v8 : ('type/pair/prod' A B), l2 : ('type/list/list' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v8 (^[a2 : A, b2 : B]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v6 (^[a1 : A, b1 : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a1 a2) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) (merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) l1 (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2))))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) (merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) l1 l2)))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) (merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) l2)))))))))))))))))))))).
tt('thm/fmapal/merge_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/merge' A B) x x1 x2) = (('const/fmapal/merge_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) x1 x2)))))).
tt('thm/fmapal/merge_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > $o)))]: (((![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)) l)) & ((![cmp : ('type/toto/toto' A), v4 : ('type/pair/prod' A B), v5 : ('type/list/list' ('type/pair/prod' A B))]: (P cmp (('const/list/CONS' ('type/pair/prod' A B)) v4 v5) ('const/list/NIL' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), a1 : A, b1 : B, l1 : ('type/list/list' ('type/pair/prod' A B)), a2 : A, b2 : B, l2 : ('type/list/list' ('type/pair/prod' A B))]: (((((('const/toto/apto' A) cmp a1 a2) = 'const/toto/EQUAL') => (P cmp l1 l2)) & ((((('const/toto/apto' A) cmp a1 a2) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) l2)) & (((('const/toto/apto' A) cmp a1 a2) = 'const/toto/LESS') => (P cmp l1 (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2))))) => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B)), v2 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1 v2))))).
tt('thm/fmapal/merge_0', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/merge' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) l) = l))).
tt('thm/fmapal/merge_1', ax, ![A : $t, B : $t]: (![v5 : ('type/list/list' ('type/pair/prod' A B)), v4 : ('type/pair/prod' A B), cmp : ('type/toto/toto' A)]: ((('const/fmapal/merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) v4 v5) ('const/list/NIL' ('type/pair/prod' A B))) = (('const/list/CONS' ('type/pair/prod' A B)) v4 v5)))).
tt('thm/fmapal/merge_e2', ax, ![A : $t, B : $t]: (![l2 : ('type/list/list' ('type/pair/prod' A B)), l1 : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b2 : B, b1 : B, a2 : A, a1 : A]: ((('const/fmapal/merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2)) = (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a1 a2) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) (('const/fmapal/merge' A B) cmp l1 (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) l2))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) (('const/fmapal/merge' A B) cmp l1 l2)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a2 b2) (('const/fmapal/merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a1 b1) l1) l2)))))).
tt('thm/fmapal/incr_merge_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/incr_merge_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))) R) & (![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/fmapal/merge' A B) cmp l m) lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)))))))) (^[incr_merge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) v1 (^[l : ('type/list/list' ('type/pair/prod' A B)), v3 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) v3 (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) l) ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) (^[v4 : ('type/option/option' ('type/list/list' ('type/pair/prod' A B))), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/option/option_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) v4 (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) l) lol)) (^[m : ('type/list/list' ('type/pair/prod' A B))]: (('const/combin/I' ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) (incr_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/fmapal/merge' A B) cmp l m) lol))))))))))))))))).
tt('thm/fmapal/incr_merge_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((('const/fmapal/incr_merge' A B) x x1 x2) = (('const/fmapal/incr_merge_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) x1 x2)))))).
tt('thm/fmapal/incr_merge_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > $o)))]: (((![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: (P cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) & ((![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol))) & (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((P cmp (('const/fmapal/merge' A B) cmp l m) lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B)), v2 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (P v v1 v2))))).
tt('thm/fmapal/incr_merge_0', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/incr_merge' A B) cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) = (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) l) ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))))).
tt('thm/fmapal/incr_merge_1', ax, ![A : $t, B : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/incr_merge' A B) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)) = (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) l) lol)))).
tt('thm/fmapal/incr_merge_e2', ax, ![A : $t, B : $t]: (![m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/incr_merge' A B) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)) = (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) (('const/fmapal/incr_merge' A B) cmp (('const/fmapal/merge' A B) cmp l m) lol))))).
tt('thm/fmapal/ORL_sublists_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_sublists_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) R) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp lol) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)))) & (![m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp lol) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)))))))) (^[ORL_sublists_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))) $o) v1 (('const/combin/I' $o) $true) (^[v2 : ('type/option/option' ('type/list/list' ('type/pair/prod' A B))), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/option/option_CASE' ('type/list/list' ('type/pair/prod' A B)) $o) v2 (('const/combin/I' $o) (ORL_sublists_tupled (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp lol))) (^[m : ('type/list/list' ('type/pair/prod' A B))]: (('const/combin/I' $o) ((('const/fmapal/ORL' A B) cmp m) & (ORL_sublists_tupled (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) cmp lol)))))))))))))).
tt('thm/fmapal/ORL_sublists_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((('const/fmapal/ORL_sublists' A B) x x1) = (('const/fmapal/ORL_sublists_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) x x1))))).
tt('thm/fmapal/ORL_sublists_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) & ((![cmp : ('type/toto/toto' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((P cmp lol) => (P cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)))) & (![cmp : ('type/toto/toto' A), m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((P cmp lol) => (P cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (P v v1))))).
tt('thm/fmapal/ORL_sublists_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_sublists' A B) cmp ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) = $true))).
tt('thm/fmapal/ORL_sublists_1', ax, ![A : $t, B : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_sublists' A B) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)) = (('const/fmapal/ORL_sublists' A B) cmp lol)))).
tt('thm/fmapal/ORL_sublists_e2', ax, ![A : $t, B : $t]: (![m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_sublists' A B) cmp (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)) = ((('const/fmapal/ORL' A B) cmp m) & (('const/fmapal/ORL_sublists' A B) cmp lol))))).
tt('thm/fmapal/incr_build_0', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/incr_build' A B) cmp ('const/list/NIL' ('type/pair/prod' A B))) = ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))).
tt('thm/fmapal/incr_build_e1', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), ab : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/incr_build' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) ab l)) = (('const/fmapal/incr_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) ab ('const/list/NIL' ('type/pair/prod' A B))) (('const/fmapal/incr_build' A B) cmp l))))).
tt('thm/fmapal/merge_out_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/merge_out_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))) R) & ((![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) l lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol))))) & (![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/fmapal/merge' A B) cmp l m) lol)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol))))))))) (^[merge_out_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) v1 (^[l : ('type/list/list' ('type/pair/prod' A B)), v3 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))) ('type/list/list' ('type/pair/prod' A B))) v3 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) l) (^[v4 : ('type/option/option' ('type/list/list' ('type/pair/prod' A B))), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (('const/option/option_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) v4 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (merge_out_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) l lol)))) (^[m : ('type/list/list' ('type/pair/prod' A B))]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (merge_out_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) (('const/fmapal/merge' A B) cmp l m) lol)))))))))))))))).
tt('thm/fmapal/merge_out_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((('const/fmapal/merge_out' A B) x x1 x2) = (('const/fmapal/merge_out_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) x1 x2)))))).
tt('thm/fmapal/merge_out_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) > $o)))]: (((![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: (P cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))))) & ((![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((P cmp l lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)))) & (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((P cmp (('const/fmapal/merge' A B) cmp l m) lol) => (P cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B)), v2 : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: (P v v1 v2))))).
tt('thm/fmapal/merge_out_0', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/merge_out' A B) cmp l ('const/list/NIL' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))) = l))).
tt('thm/fmapal/merge_out_1', ax, ![A : $t, B : $t]: (![lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/merge_out' A B) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) ('const/option/NONE' ('type/list/list' ('type/pair/prod' A B))) lol)) = (('const/fmapal/merge_out' A B) cmp l lol)))).
tt('thm/fmapal/merge_out_e2', ax, ![A : $t, B : $t]: (![m : ('type/list/list' ('type/pair/prod' A B)), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/merge_out' A B) cmp l (('const/list/CONS' ('type/option/option' ('type/list/list' ('type/pair/prod' A B)))) (('const/option/SOME' ('type/list/list' ('type/pair/prod' A B))) m) lol)) = (('const/fmapal/merge_out' A B) cmp (('const/fmapal/merge' A B) cmp l m) lol)))).
tt('thm/fmapal/incr_flat_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), lol : ('type/list/list' ('type/option/option' ('type/list/list' ('type/pair/prod' A B))))]: ((('const/fmapal/incr_flat' A B) cmp lol) = (('const/fmapal/merge_out' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) lol)))).
tt('thm/fmapal/incr_sort_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/incr_sort' A B) cmp l) = (('const/fmapal/merge_out' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) (('const/fmapal/incr_build' A B) cmp l))))).
tt('thm/fmapal/OPTION_FLAT_primitive_', def, ![Z : $t]: (('const/fmapal/OPTION_FLAT' Z) = (('const/relation/WFREC' ('type/list/list' ('type/option/option' ('type/list/list' Z))) ('type/list/list' Z)) (('const/min/@' (('type/list/list' ('type/option/option' ('type/list/list' Z))) > (('type/list/list' ('type/option/option' ('type/list/list' Z))) > $o))) (^[R : (('type/list/list' ('type/option/option' ('type/list/list' Z))) > (('type/list/list' ('type/option/option' ('type/list/list' Z))) > $o))]: ((('const/relation/WF' ('type/list/list' ('type/option/option' ('type/list/list' Z)))) R) & ((![l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: (R l (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) ('const/option/NONE' ('type/list/list' Z)) l))) & (![a : ('type/list/list' Z), l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: (R l (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) (('const/option/SOME' ('type/list/list' Z)) a) l))))))) (^[OPTION_FLAT : (('type/list/list' ('type/option/option' ('type/list/list' Z))) > ('type/list/list' Z)), 'a\'' : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: (('const/list/list_CASE' ('type/option/option' ('type/list/list' Z)) ('type/list/list' Z)) 'a\'' (('const/combin/I' ('type/list/list' Z)) ('const/list/NIL' Z)) (^[v : ('type/option/option' ('type/list/list' Z)), l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: (('const/option/option_CASE' ('type/list/list' Z) ('type/list/list' Z)) v (('const/combin/I' ('type/list/list' Z)) (OPTION_FLAT l)) (^[a : ('type/list/list' Z)]: (('const/combin/I' ('type/list/list' Z)) (('const/list/APPEND' Z) a (OPTION_FLAT l))))))))))).
tt('thm/fmapal/OPTION_FLAT_ind_', ax, ![Z : $t]: (![P : (('type/list/list' ('type/option/option' ('type/list/list' Z))) > $o)]: (((P ('const/list/NIL' ('type/option/option' ('type/list/list' Z)))) & ((![l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: ((P l) => (P (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) ('const/option/NONE' ('type/list/list' Z)) l)))) & (![a : ('type/list/list' Z), l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: ((P l) => (P (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) (('const/option/SOME' ('type/list/list' Z)) a) l)))))) => (![v : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: (P v))))).
tt('thm/fmapal/OPTION_FLAT_0', ax, ![Z : $t]: ((('const/fmapal/OPTION_FLAT' Z) ('const/list/NIL' ('type/option/option' ('type/list/list' Z)))) = ('const/list/NIL' Z))).
tt('thm/fmapal/OPTION_FLAT_1', ax, ![Z : $t]: (![l : ('type/list/list' ('type/option/option' ('type/list/list' Z)))]: ((('const/fmapal/OPTION_FLAT' Z) (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) ('const/option/NONE' ('type/list/list' Z)) l)) = (('const/fmapal/OPTION_FLAT' Z) l)))).
tt('thm/fmapal/OPTION_FLAT_e2', ax, ![Z : $t]: (![l : ('type/list/list' ('type/option/option' ('type/list/list' Z))), a : ('type/list/list' Z)]: ((('const/fmapal/OPTION_FLAT' Z) (('const/list/CONS' ('type/option/option' ('type/list/list' Z))) (('const/option/SOME' ('type/list/list' Z)) a) l)) = (('const/list/APPEND' Z) a (('const/fmapal/OPTION_FLAT' Z) l))))).
tt('thm/fmapal/unlookup_', def, ![A : $t, B : $t]: (![f : (A > ('type/option/option' B))]: ((('const/fmapal/unlookup' A B) f) = (('const/finite_map/FUN_FMAP' A B) (('const/combin/o' A B ('type/option/option' B)) ('const/option/THE' B) f) (('const/combin/o' A $o ('type/option/option' B)) ('const/option/IS_SOME' B) f))))).
tt('thm/fmapal/bt_to_fmap_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_fmap_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) ('type/finite_map/fmap' A B)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))) R) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), v : B, x : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp l) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x v) r)))) & (![v : B, x : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp r) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x v) r)))))))) (^[bt_to_fmap_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > ('type/finite_map/fmap' A B)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/finite_map/fmap' A B) ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) a (^[cmp : ('type/toto/toto' A), v2 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/finite_map/fmap' A B)) v2 (('const/combin/I' ('type/finite_map/fmap' A B)) ('const/finite_map/FEMPTY' A B)) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v4 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/finite_map/fmap' A B) A B) v4 (^[x : A, v : B]: (('const/combin/I' ('type/finite_map/fmap' A B)) (('const/finite_map/FUNION' A B) (('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) (bt_to_fmap_tupled (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp l)) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/toto/apto' A) cmp y x) = 'const/toto/LESS'))))) (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) x v))) (('const/finite_map/DRESTRICT' A B) (bt_to_fmap_tupled (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) cmp r)) (('const/pred_set/GSPEC' A A) (^[z : A]: (('const/pair/,' A $o) z ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS'))))))))))))))))).
tt('thm/fmapal/bt_to_fmap_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/FMAPAL' A B) x x1) = (('const/fmapal/bt_to_fmap_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) x x1))))).
tt('thm/fmapal/bt_to_fmap_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, v : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (((P cmp l) & (P cmp r)) => (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x v) r))))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P v v1))))).
tt('thm/fmapal/bt_to_fmap_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/FMAPAL' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B))) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/fmapal/bt_to_fmap_e1', ax, ![A : $t, B : $t]: (![x : A, v : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/FMAPAL' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x v) r)) = (('const/finite_map/FUNION' A B) (('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp l) (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y ((('const/toto/apto' A) cmp y x) = 'const/toto/LESS'))))) (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) x v))) (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp r) (('const/pred_set/GSPEC' A A) (^[z : A]: (('const/pair/,' A $o) z ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS'))))))))).
tt('thm/fmapal/FAPPLY_nt_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), x : A]: ((('const/finite_map/FAPPLY' A B) (('const/fmapal/FMAPAL' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B))) x) = (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) x)))).
tt('thm/fmapal/FAPPLY_node_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), x : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), a : A, b : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/finite_map/FAPPLY' A B) (('const/fmapal/FMAPAL' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) a b) r)) x) = (('const/toto/cpn_CASE' B) (('const/toto/apto' A) cmp x a) (('const/finite_map/FAPPLY' A B) (('const/fmapal/FMAPAL' A B) cmp l) x) b (('const/finite_map/FAPPLY' A B) (('const/fmapal/FMAPAL' A B) cmp r) x))))).
tt('thm/fmapal/bt_to_fmap_lb_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), lb : A, t : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_fmap_lb' A B) cmp lb t) = (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')))))))).
tt('thm/fmapal/bt_to_fmap_ub_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: ((('const/fmapal/bt_to_fmap_ub' A B) cmp t ub) = (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')))))))).
tt('thm/fmapal/bt_to_fmap_lb_ub_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), lb : A, t : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: ((('const/fmapal/bt_to_fmap_lb_ub' A B) cmp lb t ub) = (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))))))))).
tt('thm/fmapal/bt_map_0', def, ![B : $t, A : $t]: (![f : (A > B)]: ((('const/fmapal/bt_map' A B) f ('const/enumeral/nt' A)) = ('const/enumeral/nt' B)))).
tt('thm/fmapal/bt_map_e1', def, ![A : $t, B : $t]: (![f : (A > B), l : ('type/enumeral/bt' A), x : A, r : ('type/enumeral/bt' A)]: ((('const/fmapal/bt_map' A B) f (('const/enumeral/node' A) l x r)) = (('const/enumeral/node' B) (('const/fmapal/bt_map' A B) f l) (f x) (('const/fmapal/bt_map' A B) f r))))).
tt('thm/fmapal/bt_FST_FDOM_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp t)) = (('const/enumeral/ENUMERAL' A) cmp (('const/fmapal/bt_map' ('type/pair/prod' A B) A) ('const/pair/FST' A B) t))))).
tt('thm/fmapal/bt_to_orl_lb_ub_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_lb_ub_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)))) R) & ((![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))))) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & (~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l ub))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))))) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))))) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))))))))))) (^[bt_to_orl_lb_ub_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) v1 (^[lb : A, v3 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) A) v3 (^[v4 : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v4 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v7 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v7 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (bt_to_orl_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x)))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (bt_to_orl_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub))))) (bt_to_orl_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l ub))))) (bt_to_orl_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub)))))))))))))))))))).
tt('thm/fmapal/bt_to_orl_lb_ub_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B)), x3 : A]: ((('const/fmapal/bt_to_orl_lb_ub' A B) x x1 x2 x3) = (('const/fmapal/bt_to_orl_lb_ub_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) x (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x1 (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) x2 x3))))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o))))]: (((![cmp : ('type/toto/toto' A), lb : A, ub : A]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub)) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: ((((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (P cmp lb r ub)) & (((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & (~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))) => (P cmp lb l ub)) & (((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp lb l x)) & ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp x r ub))))) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : A]: (P v v1 v2 v3))))).
tt('thm/fmapal/bt_to_orl_lb_ub_0', ax, ![A : $t, B : $t]: (![ub : A, lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/bt_to_orl_lb_ub_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp x r ub)) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb l ub)) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb r ub))))).
tt('thm/fmapal/bt_to_orl_lb_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_lb_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B))))) R) & ((![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) lb r)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)))))) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x r)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)))))))))) (^[bt_to_orl_lb_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/enumeral/bt' ('type/pair/prod' A B))) v1 (^[lb : A, v3 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v3 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v5 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (bt_to_orl_lb_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x r)))) (bt_to_orl_lb_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) lb r))))))))))))))))).
tt('thm/fmapal/bt_to_orl_lb_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl_lb' A B) x x1 x2) = (('const/fmapal/bt_to_orl_lb_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) x (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x1 x2)))))).
tt('thm/fmapal/bt_to_orl_lb_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o)))]: (((![cmp : ('type/toto/toto' A), lb : A]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (P cmp lb r)) & (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') => (P cmp x r))) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r))))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P v v1 v2))))).
tt('thm/fmapal/bt_to_orl_lb_0', ax, ![A : $t, B : $t]: (![lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B))) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/bt_to_orl_lb_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp lb l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb' A B) cmp x r)) (('const/fmapal/bt_to_orl_lb' A B) cmp lb r))))).
tt('thm/fmapal/bt_to_orl_ub_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_ub_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) R) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l ub)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub))))) & (![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub))))))))) (^[bt_to_orl_ub_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) A) v1 (^[v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v5 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (bt_to_orl_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp x r ub)) (bt_to_orl_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l ub))))))))))))))))).
tt('thm/fmapal/bt_to_orl_ub_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B)), x2 : A]: ((('const/fmapal/bt_to_orl_ub' A B) x x1 x2) = (('const/fmapal/bt_to_orl_ub_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) x1 x2)))))).
tt('thm/fmapal/bt_to_orl_ub_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o)))]: (((![cmp : ('type/toto/toto' A), ub : A]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub)) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: ((((~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp l ub)) & (((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') => (P cmp l x))) => (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B)), v2 : A]: (P v v1 v2))))).
tt('thm/fmapal/bt_to_orl_ub_0', ax, ![A : $t, B : $t]: (![ub : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ub' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/bt_to_orl_ub_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ub' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_ub' A B) cmp l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb_ub' A B) cmp x r ub)) (('const/fmapal/bt_to_orl_ub' A B) cmp l ub))))).
tt('thm/fmapal/bt_to_orl_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))) R))) (^[bt_to_orl_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v1 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v3 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_ub' A B) cmp l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb' A B) cmp x r))))))))))))).
tt('thm/fmapal/bt_to_orl_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl' A B) x x1) = (('const/fmapal/bt_to_orl_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) x x1))))).
tt('thm/fmapal/bt_to_orl_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P v v1))))).
tt('thm/fmapal/bt_to_orl_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B))) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/bt_to_orl_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) = (('const/list/APPEND' ('type/pair/prod' A B)) (('const/list/APPEND' ('type/pair/prod' A B)) (('const/fmapal/bt_to_orl_ub' A B) cmp l x) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)))) (('const/fmapal/bt_to_orl_lb' A B) cmp x r))))).
tt('thm/fmapal/fmap_', def, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/fmap' A B) l) = (('const/finite_map/FUPDATE_LIST' A B) ('const/finite_map/FEMPTY' A B) (('const/list/REVERSE' ('type/pair/prod' A B)) l))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_tupled_AUX_', def, ![A : $t, B : $t]: (![R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > $o))]: ((('const/fmapal/bt_to_orl_lb_ub_ac_tupled_aux' A B) R) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) ('type/list/list' ('type/pair/prod' A B))) R (^[bt_to_orl_lb_ub_ac_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) v1 (^[lb : A, v3 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) v3 (^[v4 : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/list/list' ('type/pair/prod' A B))) v5 (^[ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v4 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) m) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v9 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v9 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (bt_to_orl_lb_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (bt_to_orl_lb_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) r (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m))))))))))) (bt_to_orl_lb_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))) (bt_to_orl_lb_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) r (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))))))))))))))))))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_lb_ub_ac_tupled' A B) = (('const/fmapal/bt_to_orl_lb_ub_ac_tupled_aux' A B) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))))) R) & ((![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) r (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m))))))) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & (~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m))))))) & ((![m : ('type/list/list' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac_tupled_aux' A B) R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) r (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))))))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m))))))) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, lb : A, cmp : ('type/toto/toto' A)]: ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) r (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))))))))))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B)), x3 : A, x4 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl_lb_ub_ac' A B) x x1 x2 x3 x4) = (('const/fmapal/bt_to_orl_lb_ub_ac_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) x (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) x1 (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) x2 (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x3 x4)))))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > (('type/list/list' ('type/pair/prod' A B)) > $o)))))]: (((![cmp : ('type/toto/toto' A), lb : A, ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub m)) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: ((((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (P cmp lb r ub m)) & (((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & (~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS'))) => (P cmp lb l ub m)) & (((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp lb l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m)))) & ((((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') & ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp x r ub m))))) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub m)))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : A, v4 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1 v2 v3 v4))))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_0', ax, ![A : $t, B : $t]: (![ub : A, m : ('type/list/list' ('type/pair/prod' A B)), lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub m) = m))).
tt('thm/fmapal/bt_to_orl_lb_ub_ac_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub m) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m))) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb l ub m)) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb r ub m))))).
tt('thm/fmapal/bt_to_orl_lb_ac_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_lb_ac_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))))) R) & ((![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) r m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m)))))) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, lb : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) r m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m)))))))))) (^[bt_to_orl_lb_ac_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) v1 (^[lb : A, v3 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) v3 (^[v4 : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v4 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) m) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v7 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v7 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (bt_to_orl_lb_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) r m)))))) (bt_to_orl_lb_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) r m)))))))))))))))))))).
tt('thm/fmapal/bt_to_orl_lb_ac_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B)), x3 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl_lb_ac' A B) x x1 x2 x3) = (('const/fmapal/bt_to_orl_lb_ac_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) x1 (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) x2 x3))))))).
tt('thm/fmapal/bt_to_orl_lb_ac_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > $o))))]: (((![cmp : ('type/toto/toto' A), lb : A, m : ('type/list/list' ('type/pair/prod' A B))]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) m)) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B))]: ((((~ ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS')) => (P cmp lb r m)) & (((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') => (P cmp x r m))) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m)))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1 v2 v3))))).
tt('thm/fmapal/bt_to_orl_lb_ac_0', ax, ![A : $t, B : $t]: (![m : ('type/list/list' ('type/pair/prod' A B)), lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ac' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) m) = m))).
tt('thm/fmapal/bt_to_orl_lb_ac_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_lb_ac' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp lb x) = 'const/toto/LESS') (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp lb l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ac' A B) cmp x r m))) (('const/fmapal/bt_to_orl_lb_ac' A B) cmp lb r m))))).
tt('thm/fmapal/bt_to_orl_ub_ac_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_ub_ac_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))) R) & ((![r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, cmp : ('type/toto/toto' A)]: ((~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))) & (![m : ('type/list/list' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m))))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))))))) (^[bt_to_orl_ub_ac_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) v1 (^[v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A ('type/list/list' ('type/pair/prod' A B))) v3 (^[ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) m) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v7 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v7 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (bt_to_orl_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m)))))) (bt_to_orl_ub_ac_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) l (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) ub m)))))))))))))))))))).
tt('thm/fmapal/bt_to_orl_ub_ac_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B)), x2 : A, x3 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl_ub_ac' A B) x x1 x2 x3) = (('const/fmapal/bt_to_orl_ub_ac_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A ('type/list/list' ('type/pair/prod' A B)))) x1 (('const/pair/,' A ('type/list/list' ('type/pair/prod' A B))) x2 x3))))))).
tt('thm/fmapal/bt_to_orl_ub_ac_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > (('type/list/list' ('type/pair/prod' A B)) > $o))))]: (((![cmp : ('type/toto/toto' A), ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub m)) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A, m : ('type/list/list' ('type/pair/prod' A B))]: ((((~ ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS')) => (P cmp l ub m)) & (((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') => (P cmp l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m))))) => (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub m)))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B)), v2 : A, v3 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1 v2 v3))))).
tt('thm/fmapal/bt_to_orl_ub_ac_0', ax, ![A : $t, B : $t]: (![ub : A, m : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ub_ac' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub m) = m))).
tt('thm/fmapal/bt_to_orl_ub_ac_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ub_ac' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub m) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) ((('const/toto/apto' A) cmp x ub) = 'const/toto/LESS') (('const/fmapal/bt_to_orl_ub_ac' A B) cmp l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ub_ac' A B) cmp x r ub m))) (('const/fmapal/bt_to_orl_ub_ac' A B) cmp l ub m))))).
tt('thm/fmapal/bt_to_orl_ac_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_to_orl_ac_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))) R))) (^[bt_to_orl_ac_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) v1 (^[v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) m) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v5 (^[x : A, y : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/fmapal/bt_to_orl_ub_ac' A B) cmp l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ac' A B) cmp x r m)))))))))))))))).
tt('thm/fmapal/bt_to_orl_ac_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B)), x2 : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl_ac' A B) x x1 x2) = (('const/fmapal/bt_to_orl_ac_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)))) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B))) x1 x2)))))).
tt('thm/fmapal/bt_to_orl_ac_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (('type/list/list' ('type/pair/prod' A B)) > $o)))]: (((![cmp : ('type/toto/toto' A), m : ('type/list/list' ('type/pair/prod' A B))]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)) m)) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B))]: (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B)), v2 : ('type/list/list' ('type/pair/prod' A B))]: (P v v1 v2))))).
tt('thm/fmapal/bt_to_orl_ac_0', ax, ![A : $t, B : $t]: (![m : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ac' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B)) m) = m))).
tt('thm/fmapal/bt_to_orl_ac_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), m : ('type/list/list' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_to_orl_ac' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) m) = (('const/fmapal/bt_to_orl_ub_ac' A B) cmp l x (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) (('const/fmapal/bt_to_orl_lb_ac' A B) cmp x r m)))))).
tt('thm/fmapal/ORWL_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), f : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORWL' A B) cmp f l) = ((f = (('const/fmapal/fmap' A B) l)) & (('const/fmapal/ORL' A B) cmp l))))).
tt('thm/fmapal/ORWL_bt_to_orl_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/fmapal/ORWL' A B) cmp (('const/fmapal/FMAPAL' A B) cmp t) (('const/fmapal/bt_to_orl' A B) cmp t)))).
tt('thm/fmapal/OFU_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/fmapal/OFU' A B) cmp f g) = (('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/enumeral/LESS_ALL' A) cmp x (('const/finite_map/FDOM' A B) g)))))) g)))).
tt('thm/fmapal/UFO_', def, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/fmapal/UFO' A B) cmp f g) = (('const/finite_map/FUNION' A B) f (('const/finite_map/DRESTRICT' A B) g (('const/pred_set/GSPEC' A A) (^[y : A]: (('const/pair/,' A $o) y (![z : A]: ((('const/bool/IN' A) z (('const/finite_map/FDOM' A B) f)) => ((('const/toto/apto' A) cmp z y) = 'const/toto/LESS'))))))))))).
tt('thm/fmapal/bl_to_fmap_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bl_to_fmap_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) ('type/finite_map/fmap' A B)) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B)))) R) & ((![b : ('type/enumeral/bl' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp b) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp (('const/enumeral/zerbl' ('type/pair/prod' A B)) b)))) & (![t : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, x : A, b : ('type/enumeral/bl' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp b) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp (('const/enumeral/onebl' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) t b)))))))) (^[bl_to_fmap_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) > ('type/finite_map/fmap' A B)), a : ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' ('type/finite_map/fmap' A B) ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/enumeral/bl' ('type/pair/prod' A B))]: (('const/enumeral/bl_CASE' ('type/pair/prod' A B) ('type/finite_map/fmap' A B)) v1 (('const/combin/I' ('type/finite_map/fmap' A B)) ('const/finite_map/FEMPTY' A B)) (^[b : ('type/enumeral/bl' ('type/pair/prod' A B))]: (('const/combin/I' ('type/finite_map/fmap' A B)) (bl_to_fmap_tupled (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp b)))) (^[v3 : ('type/pair/prod' A B), t : ('type/enumeral/bt' ('type/pair/prod' A B)), 'b\'' : ('type/enumeral/bl' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/finite_map/fmap' A B) A B) v3 (^[x : A, y : B]: (('const/combin/I' ('type/finite_map/fmap' A B)) (('const/fmapal/OFU' A B) cmp (('const/finite_map/FUNION' A B) (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) x y)) (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pred_set/GSPEC' A A) (^[z : A]: (('const/pair/,' A $o) z ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS')))))) (bl_to_fmap_tupled (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) cmp 'b\'')))))))))))))).
tt('thm/fmapal/bl_to_fmap_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bl' ('type/pair/prod' A B))]: ((('const/fmapal/bl_to_fmap' A B) x x1) = (('const/fmapal/bl_to_fmap_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bl' ('type/pair/prod' A B))) x x1))))).
tt('thm/fmapal/bl_to_fmap_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bl' ('type/pair/prod' A B)) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/enumeral/nbl' ('type/pair/prod' A B)))) & ((![cmp : ('type/toto/toto' A), b : ('type/enumeral/bl' ('type/pair/prod' A B))]: ((P cmp b) => (P cmp (('const/enumeral/zerbl' ('type/pair/prod' A B)) b)))) & (![cmp : ('type/toto/toto' A), x : A, y : B, t : ('type/enumeral/bt' ('type/pair/prod' A B)), b : ('type/enumeral/bl' ('type/pair/prod' A B))]: ((P cmp b) => (P cmp (('const/enumeral/onebl' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) t b)))))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bl' ('type/pair/prod' A B))]: (P v v1))))).
tt('thm/fmapal/bl_to_fmap_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/bl_to_fmap' A B) cmp ('const/enumeral/nbl' ('type/pair/prod' A B))) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/fmapal/bl_to_fmap_1', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), b : ('type/enumeral/bl' ('type/pair/prod' A B))]: ((('const/fmapal/bl_to_fmap' A B) cmp (('const/enumeral/zerbl' ('type/pair/prod' A B)) b)) = (('const/fmapal/bl_to_fmap' A B) cmp b)))).
tt('thm/fmapal/bl_to_fmap_e2', ax, ![A : $t, B : $t]: (![y : B, x : A, t : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : ('type/enumeral/bl' ('type/pair/prod' A B))]: ((('const/fmapal/bl_to_fmap' A B) cmp (('const/enumeral/onebl' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) t b)) = (('const/fmapal/OFU' A B) cmp (('const/finite_map/FUNION' A B) (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) x y)) (('const/finite_map/DRESTRICT' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pred_set/GSPEC' A A) (^[z : A]: (('const/pair/,' A $o) z ((('const/toto/apto' A) cmp x z) = 'const/toto/LESS')))))) (('const/fmapal/bl_to_fmap' A B) cmp b))))).
tt('thm/fmapal/bt_to_orl_ID_IMP_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp l) => ((('const/fmapal/bt_to_orl' A B) cmp (('const/enumeral/list_to_bt' ('type/pair/prod' A B)) l)) = l)))).
tt('thm/fmapal/fmap_FDOM_', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) l)) = (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l))))).
tt('thm/fmapal/ORL_FUNION_IMP_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp l) => (![m : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp m) => ((('const/fmapal/ORL' A B) cmp (('const/fmapal/merge' A B) cmp l m)) & ((('const/fmapal/fmap' A B) (('const/fmapal/merge' A B) cmp l m)) = (('const/finite_map/FUNION' A B) (('const/fmapal/fmap' A B) l) (('const/fmapal/fmap' A B) m))))))))).
tt('thm/fmapal/FMAPAL_FDOM_THM_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B))))) = $false))).
tt('thm/fmapal/FMAPAL_FDOM_THM_e1', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), x : A, a : A, b : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) a b) r)))) = (('const/toto/cpn_CASE' $o) (('const/toto/apto' A) cmp x a) (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp l))) $true (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp r))))))).
tt('thm/fmapal/inter_merge_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/inter_merge_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)))) R) & ((![b : B, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)))))) & ((![m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), b : B, y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)))))) & (![b : B, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l (('const/list/CONS' A) y m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m))))))))))) (^[inter_merge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > ('type/list/list' ('type/pair/prod' A B))), 'a\'' : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) 'a\'' (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) v1 (^[v2 : ('type/list/list' ('type/pair/prod' A B)), v3 : ('type/list/list' A)]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[v4 : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/list/list_CASE' A ('type/list/list' ('type/pair/prod' A B))) v3 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[y : A, m : ('type/list/list' A)]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v4 (^[a : A, b : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a y) (inter_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l (('const/list/CONS' A) y m)))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) (inter_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l m)))) (inter_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m))))))))))))))))))).
tt('thm/fmapal/inter_merge_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : ('type/list/list' A)]: ((('const/fmapal/inter_merge' A B) x x1 x2) = (('const/fmapal/inter_merge_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) x1 x2)))))).
tt('thm/fmapal/inter_merge_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' A) > $o)))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), a : A, b : B, l : ('type/list/list' ('type/pair/prod' A B))]: (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), y : A, m : ('type/list/list' A)]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)) (('const/list/CONS' A) y m))) & (![cmp : ('type/toto/toto' A), a : A, b : B, l : ('type/list/list' ('type/pair/prod' A B)), y : A, m : ('type/list/list' A)]: (((((('const/toto/apto' A) cmp a y) = 'const/toto/EQUAL') => (P cmp l m)) & ((((('const/toto/apto' A) cmp a y) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m)) & (((('const/toto/apto' A) cmp a y) = 'const/toto/LESS') => (P cmp l (('const/list/CONS' A) y m))))) => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m))))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B)), v2 : ('type/list/list' A)]: (P v v1 v2))))).
tt('thm/fmapal/inter_merge_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/inter_merge' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) ('const/list/NIL' A)) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/inter_merge_1', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : B, a : A]: ((('const/fmapal/inter_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) ('const/list/NIL' A)) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/inter_merge_2', ax, ![A : $t, B : $t]: (![y : A, m : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/fmapal/inter_merge' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) (('const/list/CONS' A) y m)) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/inter_merge_e3', ax, ![A : $t, B : $t]: (![y : A, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : B, a : A]: ((('const/fmapal/inter_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)) = (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a y) (('const/fmapal/inter_merge' A B) cmp l (('const/list/CONS' A) y m)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) (('const/fmapal/inter_merge' A B) cmp l m)) (('const/fmapal/inter_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m))))).
tt('thm/fmapal/ORL_DRESTRICT_IMP_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp l) => (![m : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp m) => ((('const/fmapal/ORL' A B) cmp (('const/fmapal/inter_merge' A B) cmp l m)) & ((('const/fmapal/fmap' A B) (('const/fmapal/inter_merge' A B) cmp l m)) = (('const/finite_map/DRESTRICT' A B) (('const/fmapal/fmap' A B) l) (('const/list/LIST_TO_SET' A) m))))))))).
tt('thm/fmapal/diff_merge_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/diff_merge_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)))) R) & ((![b : B, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/EQUAL') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)))))) & ((![m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), b : B, y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)))))) & (![b : B, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), y : A, a : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp a y) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l (('const/list/CONS' A) y m))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m))))))))))) (^[diff_merge_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) > ('type/list/list' ('type/pair/prod' A B))), 'a\'' : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) 'a\'' (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) v1 (^[v2 : ('type/list/list' ('type/pair/prod' A B)), v3 : ('type/list/list' A)]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v2 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[v4 : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v4 (^[a : A, b : B]: (('const/list/list_CASE' A ('type/list/list' ('type/pair/prod' A B))) v3 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l)) (^[y : A, m : ('type/list/list' A)]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a y) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) (diff_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l (('const/list/CONS' A) y m))))) (diff_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) l m))) (diff_merge_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) cmp (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m))))))))))))))))))).
tt('thm/fmapal/diff_merge_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : ('type/list/list' A)]: ((('const/fmapal/diff_merge' A B) x x1 x2) = (('const/fmapal/diff_merge_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' A)) x1 x2)))))).
tt('thm/fmapal/diff_merge_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/list/list' ('type/pair/prod' A B)) > (('type/list/list' A) > $o)))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), a : A, b : B, l : ('type/list/list' ('type/pair/prod' A B))]: (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) ('const/list/NIL' A))) & ((![cmp : ('type/toto/toto' A), y : A, m : ('type/list/list' A)]: (P cmp ('const/list/NIL' ('type/pair/prod' A B)) (('const/list/CONS' A) y m))) & (![cmp : ('type/toto/toto' A), a : A, b : B, l : ('type/list/list' ('type/pair/prod' A B)), y : A, m : ('type/list/list' A)]: (((((('const/toto/apto' A) cmp a y) = 'const/toto/EQUAL') => (P cmp l m)) & ((((('const/toto/apto' A) cmp a y) = 'const/toto/GREATER') => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m)) & (((('const/toto/apto' A) cmp a y) = 'const/toto/LESS') => (P cmp l (('const/list/CONS' A) y m))))) => (P cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m))))))) => (![v : ('type/toto/toto' A), v1 : ('type/list/list' ('type/pair/prod' A B)), v2 : ('type/list/list' A)]: (P v v1 v2))))).
tt('thm/fmapal/diff_merge_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/diff_merge' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) ('const/list/NIL' A)) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/diff_merge_1', ax, ![A : $t, B : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : B, a : A]: ((('const/fmapal/diff_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) ('const/list/NIL' A)) = (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l)))).
tt('thm/fmapal/diff_merge_2', ax, ![A : $t, B : $t]: (![y : A, m : ('type/list/list' A), cmp : ('type/toto/toto' A)]: ((('const/fmapal/diff_merge' A B) cmp ('const/list/NIL' ('type/pair/prod' A B)) (('const/list/CONS' A) y m)) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/diff_merge_e3', ax, ![A : $t, B : $t]: (![y : A, m : ('type/list/list' A), l : ('type/list/list' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A), b : B, a : A]: ((('const/fmapal/diff_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) (('const/list/CONS' A) y m)) = (('const/toto/cpn_CASE' ('type/list/list' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp a y) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) (('const/fmapal/diff_merge' A B) cmp l (('const/list/CONS' A) y m))) (('const/fmapal/diff_merge' A B) cmp l m) (('const/fmapal/diff_merge' A B) cmp (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) a b) l) m))))).
tt('thm/fmapal/ORL_DRESTRICT_COMPL_IMP_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp l) => (![m : ('type/list/list' A)]: ((('const/enumeral/OL' A) cmp m) => ((('const/fmapal/ORL' A B) cmp (('const/fmapal/diff_merge' A B) cmp l m)) & ((('const/fmapal/fmap' A B) (('const/fmapal/diff_merge' A B) cmp l m)) = (('const/finite_map/DRESTRICT' A B) (('const/fmapal/fmap' A B) l) (('const/pred_set/COMPL' A) (('const/list/LIST_TO_SET' A) m)))))))))).
tt('thm/fmapal/FMAPAL_fmap_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/fmap' A B) l) = (('const/fmapal/FMAPAL' A B) cmp (('const/enumeral/list_to_bt' ('type/pair/prod' A B)) (('const/fmapal/incr_sort' A B) cmp l)))))).
tt('thm/fmapal/ORL_FMAPAL_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/fmapal/ORL' A B) cmp l) => ((('const/fmapal/fmap' A B) l) = (('const/fmapal/FMAPAL' A B) cmp (('const/enumeral/list_to_bt' ('type/pair/prod' A B)) l)))))).
tt('thm/fmapal/ORWL_FUNION_THM_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), s : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B)), t : ('type/finite_map/fmap' A B), m : ('type/list/list' ('type/pair/prod' A B))]: (((('const/fmapal/ORWL' A B) cmp s l) & (('const/fmapal/ORWL' A B) cmp t m)) => (('const/fmapal/ORWL' A B) cmp (('const/finite_map/FUNION' A B) s t) (('const/fmapal/merge' A B) cmp l m))))).
tt('thm/fmapal/ORWL_DRESTRICT_THM_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), s : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B)), t : (A > $o), m : ('type/list/list' A)]: (((('const/fmapal/ORWL' A B) cmp s l) & (('const/enumeral/OWL' A) cmp t m)) => (('const/fmapal/ORWL' A B) cmp (('const/finite_map/DRESTRICT' A B) s t) (('const/fmapal/inter_merge' A B) cmp l m))))).
tt('thm/fmapal/ORWL_DRESTRICT_COMPL_THM_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), s : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B)), t : (A > $o), m : ('type/list/list' A)]: (((('const/fmapal/ORWL' A B) cmp s l) & (('const/enumeral/OWL' A) cmp t m)) => (('const/fmapal/ORWL' A B) cmp (('const/finite_map/DRESTRICT' A B) s (('const/pred_set/COMPL' A) t)) (('const/fmapal/diff_merge' A B) cmp l m))))).
tt('thm/fmapal/AP_SND_', def, ![B : $t, C : $t, A : $t]: (![f : (B > C), a : A, b : B]: ((('const/fmapal/AP_SND' A B C) f (('const/pair/,' A B) a b)) = (('const/pair/,' A C) a (f b))))).
tt('thm/fmapal/o_f_bt_map_', ax, ![A : $t, B : $t, C : $t]: (![cmp : ('type/toto/toto' A), f : (B > C), t : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/finite_map/o_f' A B C) f (('const/fmapal/FMAPAL' A B) cmp t)) = (('const/fmapal/FMAPAL' A C) cmp (('const/fmapal/bt_map' ('type/pair/prod' A B) ('type/pair/prod' A C)) (('const/fmapal/AP_SND' A B C) f) t))))).
tt('thm/fmapal/FAPPLY_fmap_NIL_', ax, ![A : $t, B : $t]: (![x : A]: ((('const/finite_map/FAPPLY' A B) (('const/fmapal/fmap' A B) ('const/list/NIL' ('type/pair/prod' A B))) x) = (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) x)))).
tt('thm/fmapal/FAPPLY_fmap_CONS_', ax, ![A : $t, B : $t]: (![x : A, y : A, z : B, l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/finite_map/FAPPLY' A B) (('const/fmapal/fmap' A B) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) y z) l)) x) = (('const/bool/COND' B) (x = y) z (('const/finite_map/FAPPLY' A B) (('const/fmapal/fmap' A B) l) x))))).
tt('thm/fmapal/o_f_fmap_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/finite_map/o_f' A B C) f (('const/fmapal/fmap' A B) l)) = (('const/fmapal/fmap' A C) (('const/list/MAP' ('type/pair/prod' A B) ('type/pair/prod' A C)) (('const/fmapal/AP_SND' A B C) f) l))))).
tt('thm/fmapal/ORL_bt_lb_ub_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_bt_lb_ub_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)))) R) & ((![ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, x : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub))))) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub))))))))) (^[ORL_bt_lb_ub_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))]: (('const/pair/pair_CASE' $o A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) v1 (^[lb : A, v3 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)]: (('const/pair/pair_CASE' $o ('type/enumeral/bt' ('type/pair/prod' A B)) A) v3 (^[v4 : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) $o) v4 (('const/combin/I' $o) ((('const/toto/apto' A) cmp lb ub) = 'const/toto/LESS')) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v7 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' $o A B) v7 (^[x : A, y : B]: (('const/combin/I' $o) ((ORL_bt_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) lb (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x)))) & (ORL_bt_lb_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) cmp (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) r ub)))))))))))))))))))).
tt('thm/fmapal/ORL_bt_lb_ub_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B)), x3 : A]: ((('const/fmapal/ORL_bt_lb_ub' A B) x x1 x2 x3) = (('const/fmapal/ORL_bt_lb_ub_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) x (('const/pair/,' A ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x1 (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) x2 x3))))))).
tt('thm/fmapal/ORL_bt_lb_ub_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o))))]: (((![cmp : ('type/toto/toto' A), lb : A, ub : A]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub)) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: (((P cmp lb l x) & (P cmp x r ub)) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : A]: (P v v1 v2 v3))))).
tt('thm/fmapal/ORL_bt_lb_ub_0', ax, ![A : $t, B : $t]: (![ub : A, lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_lb_ub' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)) ub) = ((('const/toto/apto' A) cmp lb ub) = 'const/toto/LESS')))).
tt('thm/fmapal/ORL_bt_lb_ub_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_lb_ub' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub) = ((('const/fmapal/ORL_bt_lb_ub' A B) cmp lb l x) & (('const/fmapal/ORL_bt_lb_ub' A B) cmp x r ub))))).
tt('thm/fmapal/ORL_bt_lb_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_bt_lb_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B))))) R) & (![y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x r)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)))))))) (^[ORL_bt_lb_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' $o A ('type/enumeral/bt' ('type/pair/prod' A B))) v1 (^[lb : A, v3 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) $o) v3 (('const/combin/I' $o) $true) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' $o A B) v5 (^[x : A, y : B]: (('const/combin/I' $o) ((('const/fmapal/ORL_bt_lb_ub' A B) cmp lb l x) & (ORL_bt_lb_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) cmp (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x r))))))))))))))))).
tt('thm/fmapal/ORL_bt_lb_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : A, x2 : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/ORL_bt_lb' A B) x x1 x2) = (('const/fmapal/ORL_bt_lb_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' A ('type/enumeral/bt' ('type/pair/prod' A B)))) x (('const/pair/,' A ('type/enumeral/bt' ('type/pair/prod' A B))) x1 x2)))))).
tt('thm/fmapal/ORL_bt_lb_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (A > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o)))]: (((![cmp : ('type/toto/toto' A), lb : A]: (P cmp lb ('const/enumeral/nt' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((P cmp x r) => (P cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r))))) => (![v : ('type/toto/toto' A), v1 : A, v2 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P v v1 v2))))).
tt('thm/fmapal/ORL_bt_lb_0', ax, ![A : $t, B : $t]: (![lb : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_lb' A B) cmp lb ('const/enumeral/nt' ('type/pair/prod' A B))) = $true))).
tt('thm/fmapal/ORL_bt_lb_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), lb : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_lb' A B) cmp lb (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) = ((('const/fmapal/ORL_bt_lb_ub' A B) cmp lb l x) & (('const/fmapal/ORL_bt_lb' A B) cmp x r))))).
tt('thm/fmapal/ORL_bt_ub_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_bt_ub_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))) R) & (![ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, x : A, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x)) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub))))))) (^[ORL_bt_ub_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)]: (('const/pair/pair_CASE' $o ('type/enumeral/bt' ('type/pair/prod' A B)) A) v1 (^[v2 : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) $o) v2 (('const/combin/I' $o) $true) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v5 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' $o A B) v5 (^[x : A, y : B]: (('const/combin/I' $o) ((ORL_bt_ub_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) cmp (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) l x))) & (('const/fmapal/ORL_bt_lb_ub' A B) cmp x r ub))))))))))))))).
tt('thm/fmapal/ORL_bt_ub_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B)), x2 : A]: ((('const/fmapal/ORL_bt_ub' A B) x x1 x2) = (('const/fmapal/ORL_bt_ub_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) A)) x (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) A) x1 x2)))))).
tt('thm/fmapal/ORL_bt_ub_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > (A > $o)))]: (((![cmp : ('type/toto/toto' A), ub : A]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub)) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), ub : A]: ((P cmp l x) => (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub)))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B)), v2 : A]: (P v v1 v2))))).
tt('thm/fmapal/ORL_bt_ub_0', ax, ![A : $t, B : $t]: (![ub : A, cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_ub' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B)) ub) = $true))).
tt('thm/fmapal/ORL_bt_ub_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, ub : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt_ub' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r) ub) = ((('const/fmapal/ORL_bt_ub' A B) cmp l x) & (('const/fmapal/ORL_bt_lb_ub' A B) cmp x r ub))))).
tt('thm/fmapal/ORL_bt_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/ORL_bt_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) $o) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))]: (('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))) R))) (^[ORL_bt_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) > $o), a : ('type/pair/prod' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/pair/pair_CASE' $o ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) $o) v1 (('const/combin/I' $o) $true) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v3 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' $o A B) v3 (^[x : A, y : B]: (('const/combin/I' $o) ((('const/fmapal/ORL_bt_ub' A B) cmp l x) & (('const/fmapal/ORL_bt_lb' A B) cmp x r))))))))))))).
tt('thm/fmapal/ORL_bt_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/ORL_bt' A B) x x1) = (('const/fmapal/ORL_bt_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/enumeral/bt' ('type/pair/prod' A B))) x x1))))).
tt('thm/fmapal/ORL_bt_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/enumeral/bt' ('type/pair/prod' A B)) > $o))]: (((![cmp : ('type/toto/toto' A)]: (P cmp ('const/enumeral/nt' ('type/pair/prod' A B)))) & (![cmp : ('type/toto/toto' A), l : ('type/enumeral/bt' ('type/pair/prod' A B)), x : A, y : B, r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)))) => (![v : ('type/toto/toto' A), v1 : ('type/enumeral/bt' ('type/pair/prod' A B))]: (P v v1))))).
tt('thm/fmapal/ORL_bt_0', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt' A B) cmp ('const/enumeral/nt' ('type/pair/prod' A B))) = $true))).
tt('thm/fmapal/ORL_bt_e1', ax, ![A : $t, B : $t]: (![y : B, x : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cmp : ('type/toto/toto' A)]: ((('const/fmapal/ORL_bt' A B) cmp (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) = ((('const/fmapal/ORL_bt_ub' A B) cmp l x) & (('const/fmapal/ORL_bt_lb' A B) cmp x r))))).
tt('thm/fmapal/better_bt_to_orl_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), t : ('type/enumeral/bt' ('type/pair/prod' A B))]: ((('const/fmapal/bt_to_orl' A B) cmp t) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) (('const/fmapal/ORL_bt' A B) cmp t) (('const/enumeral/bt_to_list_ac' ('type/pair/prod' A B)) t ('const/list/NIL' ('type/pair/prod' A B))) (('const/fmapal/bt_to_orl_ac' A B) cmp t ('const/list/NIL' ('type/pair/prod' A B))))))).
tt('thm/fmapal/list_rplacv_cn_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/list_rplacv_cn_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) ('type/list/list' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > $o))) (^[R : (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))) R) & (![z : B, cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))), l : ('type/list/list' ('type/pair/prod' A B)), y : B, w : A, x : A]: ((~ (x = w)) => (R (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))) l (^[m : ('type/list/list' ('type/pair/prod' A B))]: (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) m))))) (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) l) cn)))))))) (^[list_rplacv_cn_tupled : (('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) > ('type/list/list' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) a (^[v : ('type/pair/prod' A B), v1 : ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v (^[x : A, y : B]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))) v1 (^[v4 : ('type/list/list' ('type/pair/prod' A B)), cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: (('const/list/list_CASE' ('type/pair/prod' A B) ('type/list/list' ('type/pair/prod' A B))) v4 (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) ('const/list/NIL' ('type/pair/prod' A B))) (^[v6 : ('type/pair/prod' A B), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/list/list' ('type/pair/prod' A B)) A B) v6 (^[w : A, z : B]: (('const/combin/I' ('type/list/list' ('type/pair/prod' A B))) (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) (x = w) (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) l)) (list_rplacv_cn_tupled (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))) l (^[m : ('type/list/list' ('type/pair/prod' A B))]: (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) m)))))))))))))))))))))).
tt('thm/fmapal/list_rplacv_cn_curried_', def, ![A : $t, B : $t]: (![x : ('type/pair/prod' A B), x1 : ('type/list/list' ('type/pair/prod' A B)), x2 : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: ((('const/fmapal/list_rplacv_cn' A B) x x1 x2) = (('const/fmapal/list_rplacv_cn_tupled' A B) (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))))) x (('const/pair/,' ('type/list/list' ('type/pair/prod' A B)) (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))) x1 x2)))))).
tt('thm/fmapal/list_rplacv_cn_ind_', ax, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > (('type/list/list' ('type/pair/prod' A B)) > ((('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B))) > $o)))]: (((![x : A, y : B, cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: (P (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)) cn)) & (![x : A, y : B, w : A, z : B, l : ('type/list/list' ('type/pair/prod' A B)), cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: (((~ (x = w)) => (P (('const/pair/,' A B) x y) l (^[m : ('type/list/list' ('type/pair/prod' A B))]: (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) m))))) => (P (('const/pair/,' A B) x y) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) l) cn)))) => (![v : A, v1 : B, v2 : ('type/list/list' ('type/pair/prod' A B)), v3 : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: (P (('const/pair/,' A B) v v1) v2 v3))))).
tt('thm/fmapal/list_rplacv_cn_0', ax, ![A : $t, B : $t]: (![y : B, x : A, cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: ((('const/fmapal/list_rplacv_cn' A B) (('const/pair/,' A B) x y) ('const/list/NIL' ('type/pair/prod' A B)) cn) = ('const/list/NIL' ('type/pair/prod' A B))))).
tt('thm/fmapal/list_rplacv_cn_e1', ax, ![A : $t, B : $t]: (![z : B, y : B, x : A, w : A, l : ('type/list/list' ('type/pair/prod' A B)), cn : (('type/list/list' ('type/pair/prod' A B)) > ('type/list/list' ('type/pair/prod' A B)))]: ((('const/fmapal/list_rplacv_cn' A B) (('const/pair/,' A B) x y) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) l) cn) = (('const/bool/COND' ('type/list/list' ('type/pair/prod' A B))) (x = w) (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) x y) l)) (('const/fmapal/list_rplacv_cn' A B) (('const/pair/,' A B) x y) l (^[m : ('type/list/list' ('type/pair/prod' A B))]: (cn (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) m)))))))).
tt('thm/fmapal/fmap_FDOM_rec_0', ax, ![A : $t, B : $t]: (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) ('const/list/NIL' ('type/pair/prod' A B))))) = $false))).
tt('thm/fmapal/fmap_FDOM_rec_e1', ax, ![A : $t, B : $t]: (![x : A, w : A, z : B, l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) (('const/list/CONS' ('type/pair/prod' A B)) (('const/pair/,' A B) w z) l)))) = ((x = w) | (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) l))))))).
tt('thm/fmapal/list_rplacv_thm_', ax, ![A : $t, B : $t]: (![x : A, y : B, l : ('type/list/list' ('type/pair/prod' A B))]: (('const/bool/LET' ('type/list/list' ('type/pair/prod' A B)) $o) (^[ans : ('type/list/list' ('type/pair/prod' A B))]: (('const/bool/COND' $o) (ans = ('const/list/NIL' ('type/pair/prod' A B))) (~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) l)))) ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/fmap' A B) l))) & ((('const/finite_map/FUPDATE' A B) (('const/fmapal/fmap' A B) l) (('const/pair/,' A B) x y)) = (('const/fmapal/fmap' A B) ans))))) (('const/fmapal/list_rplacv_cn' A B) (('const/pair/,' A B) x y) l (^[m : ('type/list/list' ('type/pair/prod' A B))]: m))))).
tt('thm/fmapal/bt_rplacv_cn_tupled_primitive_', def, ![A : $t, B : $t]: (('const/fmapal/bt_rplacv_cn_tupled' A B) = (('const/relation/WFREC' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) ('type/enumeral/bt' ('type/pair/prod' A B))) (('const/min/@' (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > $o))) (^[R : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))))) R) & ((![z : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))), r : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, w : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x w) = 'const/toto/GREATER') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) r (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) m)))))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) r) cn)))))) & (![r : ('type/enumeral/bt' ('type/pair/prod' A B)), z : B, cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))), l : ('type/enumeral/bt' ('type/pair/prod' A B)), y : B, w : A, x : A, cmp : ('type/toto/toto' A)]: (((('const/toto/apto' A) cmp x w) = 'const/toto/LESS') => (R (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) l (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) m (('const/pair/,' A B) w z) r)))))) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) r) cn)))))))))) (^[bt_rplacv_cn_tupled : (('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) > ('type/enumeral/bt' ('type/pair/prod' A B))), a : ('type/pair/prod' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))))]: (('const/pair/pair_CASE' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) a (^[cmp : ('type/toto/toto' A), v1 : ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))]: (('const/pair/pair_CASE' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) v1 (^[v2 : ('type/pair/prod' A B), v3 : ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))]: (('const/pair/pair_CASE' ('type/enumeral/bt' ('type/pair/prod' A B)) A B) v2 (^[x : A, y : B]: (('const/pair/pair_CASE' ('type/enumeral/bt' ('type/pair/prod' A B)) ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) v3 (^[v6 : ('type/enumeral/bt' ('type/pair/prod' A B)), cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))]: (('const/enumeral/bt_CASE' ('type/pair/prod' A B) ('type/enumeral/bt' ('type/pair/prod' A B))) v6 (('const/combin/I' ('type/enumeral/bt' ('type/pair/prod' A B))) ('const/enumeral/nt' ('type/pair/prod' A B))) (^[l : ('type/enumeral/bt' ('type/pair/prod' A B)), v9 : ('type/pair/prod' A B), r : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/pair/pair_CASE' ('type/enumeral/bt' ('type/pair/prod' A B)) A B) v9 (^[w : A, z : B]: (('const/combin/I' ('type/enumeral/bt' ('type/pair/prod' A B))) (('const/toto/cpn_CASE' ('type/enumeral/bt' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp x w) (bt_rplacv_cn_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) l (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) m (('const/pair/,' A B) w z) r))))))) (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) (bt_rplacv_cn_tupled (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) cmp (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) (('const/pair/,' A B) x y) (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) r (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) m))))))))))))))))))))))))).
tt('thm/fmapal/bt_rplacv_cn_curried_', def, ![A : $t, B : $t]: (![x : ('type/toto/toto' A), x1 : ('type/pair/prod' A B), x2 : ('type/enumeral/bt' ('type/pair/prod' A B)), x3 : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))]: ((('const/fmapal/bt_rplacv_cn' A B) x x1 x2 x3) = (('const/fmapal/bt_rplacv_cn_tupled' A B) (('const/pair/,' ('type/toto/toto' A) ('type/pair/prod' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))))) x (('const/pair/,' ('type/pair/prod' A B) ('type/pair/prod' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))))) x1 (('const/pair/,' ('type/enumeral/bt' ('type/pair/prod' A B)) (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))) x2 x3))))))).
tt('thm/fmapal/bt_rplacv_cn_ind_', ax, ![A : $t, B : $t]: (![P : (('type/toto/toto' A) > (('type/pair/prod' A B) > (('type/enumeral/bt' ('type/pair/prod' A B)) > ((('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))) > $o))))]: (((![cmp : ('type/toto/toto' A), x : A, y : B, cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))]: (P cmp (('const/pair/,' A B) x y) ('const/enumeral/nt' ('type/pair/prod' A B)) cn)) & (![cmp : ('type/toto/toto' A), x : A, y : B, l : ('type/enumeral/bt' ('type/pair/prod' A B)), w : A, z : B, r : ('type/enumeral/bt' ('type/pair/prod' A B)), cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))]: (((((('const/toto/apto' A) cmp x w) = 'const/toto/GREATER') => (P cmp (('const/pair/,' A B) x y) r (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) m))))) & (((('const/toto/apto' A) cmp x w) = 'const/toto/LESS') => (P cmp (('const/pair/,' A B) x y) l (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) m (('const/pair/,' A B) w z) r)))))) => (P cmp (('const/pair/,' A B) x y) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) r) cn)))) => (![v : ('type/toto/toto' A), v1 : A, v2 : B, v3 : ('type/enumeral/bt' ('type/pair/prod' A B)), v4 : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B)))]: (P v (('const/pair/,' A B) v1 v2) v3 v4))))).
tt('thm/fmapal/bt_rplacv_cn_0', ax, ![A : $t, B : $t]: (![y : B, x : A, cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_rplacv_cn' A B) cmp (('const/pair/,' A B) x y) ('const/enumeral/nt' ('type/pair/prod' A B)) cn) = ('const/enumeral/nt' ('type/pair/prod' A B))))).
tt('thm/fmapal/bt_rplacv_cn_e1', ax, ![A : $t, B : $t]: (![z : B, y : B, x : A, w : A, r : ('type/enumeral/bt' ('type/pair/prod' A B)), l : ('type/enumeral/bt' ('type/pair/prod' A B)), cn : (('type/enumeral/bt' ('type/pair/prod' A B)) > ('type/enumeral/bt' ('type/pair/prod' A B))), cmp : ('type/toto/toto' A)]: ((('const/fmapal/bt_rplacv_cn' A B) cmp (('const/pair/,' A B) x y) (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) r) cn) = (('const/toto/cpn_CASE' ('type/enumeral/bt' ('type/pair/prod' A B))) (('const/toto/apto' A) cmp x w) (('const/fmapal/bt_rplacv_cn' A B) cmp (('const/pair/,' A B) x y) l (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) m (('const/pair/,' A B) w z) r)))) (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) x y) r)) (('const/fmapal/bt_rplacv_cn' A B) cmp (('const/pair/,' A B) x y) r (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: (cn (('const/enumeral/node' ('type/pair/prod' A B)) l (('const/pair/,' A B) w z) m)))))))).
tt('thm/fmapal/bt_rplacv_thm_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), x : A, y : B, t : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/bool/LET' ('type/enumeral/bt' ('type/pair/prod' A B)) $o) (^[ans : ('type/enumeral/bt' ('type/pair/prod' A B))]: (('const/bool/COND' $o) (ans = ('const/enumeral/nt' ('type/pair/prod' A B))) (~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp t)))) ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/fmapal/FMAPAL' A B) cmp t))) & ((('const/finite_map/FUPDATE' A B) (('const/fmapal/FMAPAL' A B) cmp t) (('const/pair/,' A B) x y)) = (('const/fmapal/FMAPAL' A B) cmp ans))))) (('const/fmapal/bt_rplacv_cn' A B) cmp (('const/pair/,' A B) x y) t (^[m : ('type/enumeral/bt' ('type/pair/prod' A B))]: m))))).
tt('thm/fmapal/FUN_fmap_thm_', ax, ![A : $t, B : $t]: (![f : (A > B), l : ('type/list/list' A)]: ((('const/fmapal/fmap' A B) (('const/list/MAP' A ('type/pair/prod' A B)) (^[x : A]: (('const/pair/,' A B) x (f x))) l)) = (('const/finite_map/FUN_FMAP' A B) f (('const/list/LIST_TO_SET' A) l))))).
tt('thm/fmapal/fmap_ORWL_thm_', ax, ![A : $t, B : $t]: (![cmp : ('type/toto/toto' A), l : ('type/list/list' ('type/pair/prod' A B))]: (('const/fmapal/ORWL' A B) cmp (('const/fmapal/fmap' A B) l) (('const/fmapal/incr_sort' A B) cmp l)))).
