tt('type/finite_map/fmap', ty, $t > $t > $t).
tt('const/finite_map/DRESTRICT', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > ((A > $o) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/FAPPLY', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (A > B))).
tt('const/finite_map/FCARD', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > 'type/num/num')).
tt('const/finite_map/FDOM', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (A > $o))).
tt('const/finite_map/FEMPTY', ty, ![A : $t, B : $t]: ('type/finite_map/fmap' A B)).
tt('const/finite_map/FEVERY', ty, ![A : $t, B : $t]: ((('type/pair/prod' A B) > $o) > (('type/finite_map/fmap' A B) > $o))).
tt('const/finite_map/FLOOKUP', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (A > ('type/option/option' B)))).
tt('const/finite_map/FMAP_MAP2', ty, ![A : $t, B : $t, C : $t]: ((('type/pair/prod' A C) > B) > (('type/finite_map/fmap' A C) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/FMERGE', ty, ![A : $t, B : $t]: ((A > (A > A)) > (('type/finite_map/fmap' B A) > (('type/finite_map/fmap' B A) > ('type/finite_map/fmap' B A))))).
tt('const/finite_map/FRANGE', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (B > $o))).
tt('const/finite_map/FUNION', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/FUN_FMAP', ty, ![A : $t, B : $t]: ((A > B) > ((A > $o) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/FUPDATE', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/pair/prod' A B) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/FUPDATE_LIST', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/list/list' ('type/pair/prod' A B)) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/MAP_KEYS', ty, ![A : $t, B : $t, C : $t]: ((A > B) > (('type/finite_map/fmap' A C) > ('type/finite_map/fmap' B C)))).
tt('const/finite_map/RRESTRICT', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > ((B > $o) > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/SUBMAP', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' A B) > $o))).
tt('const/finite_map/f_o', ty, ![A : $t, B : $t, C : $t]: (('type/finite_map/fmap' B C) > ((A > B) > ('type/finite_map/fmap' A C)))).
tt('const/finite_map/f_o_f', ty, ![A : $t, B : $t, C : $t]: (('type/finite_map/fmap' B C) > (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A C)))).
tt('const/finite_map/fdomsub', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (A > ('type/finite_map/fmap' A B)))).
tt('const/finite_map/fmap_ABS', ty, ![A : $t, B : $t]: ((A > ('type/sum/sum' B 'type/one/one')) > ('type/finite_map/fmap' A B))).
tt('const/finite_map/fmap_EQ_UPTO', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' A B) > ((A > $o) > $o)))).
tt('const/finite_map/fmap_REP', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (A > ('type/sum/sum' B 'type/one/one')))).
tt('const/finite_map/fmap_inverse', ty, ![A : $t, B : $t]: (('type/finite_map/fmap' A B) > (('type/finite_map/fmap' B A) > $o))).
tt('const/finite_map/fmap_rel', ty, ![A : $t, B : $t, C : $t]: ((A > (B > $o)) > (('type/finite_map/fmap' C A) > (('type/finite_map/fmap' C B) > $o)))).
tt('const/finite_map/fmap_size', ty, ![A : $t, B : $t]: ((A > 'type/num/num') > ((B > 'type/num/num') > (('type/finite_map/fmap' A B) > 'type/num/num')))).
tt('const/finite_map/is_fmap', ty, ![A : $t, B : $t]: ((A > ('type/sum/sum' B 'type/one/one')) > $o)).
tt('const/finite_map/o_f', ty, ![A : $t, B : $t, C : $t]: ((B > C) > (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A C)))).
tt('thm/finite_map/is_fmap_def_', def, ![A : $t, B : $t]: (('const/finite_map/is_fmap' A B) = (^[a0 : (A > ('type/sum/sum' B 'type/one/one'))]: (!['is_fmap\'' : ((A > ('type/sum/sum' B 'type/one/one')) > $o)]: ((![a00 : (A > ('type/sum/sum' B 'type/one/one'))]: (((a00 = (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one'))) | (?[f : (A > ('type/sum/sum' B 'type/one/one')), a : A, b : B]: ((a00 = (^[x : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (x = a) (('const/sum/INL' B 'type/one/one') b) (f x)))) & ('is_fmap\'' f)))) => ('is_fmap\'' a00))) => ('is_fmap\'' a0)))))).
tt('thm/finite_map/is_fmap_rules_0', ax, ![B : $t, A : $t]: (('const/finite_map/is_fmap' A B) (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one')))).
tt('thm/finite_map/is_fmap_rules_e1', ax, ![A : $t, B : $t]: (![f : (A > ('type/sum/sum' B 'type/one/one')), a : A, b : B]: ((('const/finite_map/is_fmap' A B) f) => (('const/finite_map/is_fmap' A B) (^[x : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (x = a) (('const/sum/INL' B 'type/one/one') b) (f x))))))).
tt('thm/finite_map/is_fmap_ind_', ax, ![A : $t, B : $t]: (!['is_fmap\'' : ((A > ('type/sum/sum' B 'type/one/one')) > $o)]: ((('is_fmap\'' (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one'))) & (![f : (A > ('type/sum/sum' B 'type/one/one')), a : A, b : B]: (('is_fmap\'' f) => ('is_fmap\'' (^[x : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (x = a) (('const/sum/INL' B 'type/one/one') b) (f x))))))) => (![a0 : (A > ('type/sum/sum' B 'type/one/one'))]: ((('const/finite_map/is_fmap' A B) a0) => ('is_fmap\'' a0)))))).
tt('thm/finite_map/is_fmap_strongind_', ax, ![A : $t, B : $t]: (!['is_fmap\'' : ((A > ('type/sum/sum' B 'type/one/one')) > $o)]: ((('is_fmap\'' (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one'))) & (![f : (A > ('type/sum/sum' B 'type/one/one')), a : A, b : B]: (((('const/finite_map/is_fmap' A B) f) & ('is_fmap\'' f)) => ('is_fmap\'' (^[x : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (x = a) (('const/sum/INL' B 'type/one/one') b) (f x))))))) => (![a0 : (A > ('type/sum/sum' B 'type/one/one'))]: ((('const/finite_map/is_fmap' A B) a0) => ('is_fmap\'' a0)))))).
tt('thm/finite_map/is_fmap_cases_', ax, ![A : $t, B : $t]: (![a0 : (A > ('type/sum/sum' B 'type/one/one'))]: ((('const/finite_map/is_fmap' A B) a0) = ((a0 = (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one'))) | (?[f : (A > ('type/sum/sum' B 'type/one/one')), a : A, b : B]: ((a0 = (^[x : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (x = a) (('const/sum/INL' B 'type/one/one') b) (f x)))) & (('const/finite_map/is_fmap' A B) f))))))).
tt('thm/finite_map/fmap_TY_DEF_', def, ![A : $t, B : $t]: (?[rep : (('type/finite_map/fmap' A B) > (A > ('type/sum/sum' B 'type/one/one')))]: (('const/bool/TYPE_DEFINITION' (A > ('type/sum/sum' B 'type/one/one')) ('type/finite_map/fmap' A B)) ('const/finite_map/is_fmap' A B) rep))).
tt('thm/finite_map/fmap_ISO_DEF_0', def, ![A : $t, B : $t]: (![a : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fmap_ABS' A B) (('const/finite_map/fmap_REP' A B) a)) = a))).
tt('thm/finite_map/fmap_ISO_DEF_e1', def, ![A : $t, B : $t]: (![r : (A > ('type/sum/sum' B 'type/one/one'))]: ((('const/finite_map/is_fmap' A B) r) = ((('const/finite_map/fmap_REP' A B) (('const/finite_map/fmap_ABS' A B) r)) = r)))).
tt('thm/finite_map/FUPDATE_DEF_', def, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) = (('const/finite_map/fmap_ABS' A B) (^[a : A]: (('const/bool/COND' ('type/sum/sum' B 'type/one/one')) (a = x) (('const/sum/INL' B 'type/one/one') y) (('const/finite_map/fmap_REP' A B) f a))))))).
tt('thm/finite_map/FEMPTY_DEF_', def, ![B : $t, A : $t]: (('const/finite_map/FEMPTY' A B) = (('const/finite_map/fmap_ABS' A B) (^[a : A]: (('const/sum/INR' B 'type/one/one') 'const/one/one'))))).
tt('thm/finite_map/FAPPLY_DEF_', def, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FAPPLY' A B) f x) = (('const/sum/OUTL' B 'type/one/one') (('const/finite_map/fmap_REP' A B) f x))))).
tt('thm/finite_map/FDOM_DEF_', def, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FDOM' A B) f x) = (('const/sum/ISL' B 'type/one/one') (('const/finite_map/fmap_REP' A B) f x))))).
tt('thm/finite_map/FAPPLY_FUPDATE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) x) = y))).
tt('thm/finite_map/NOT_EQ_FAPPLY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), a : A, x : A, y : B]: ((~ (a = x)) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) a) = (('const/finite_map/FAPPLY' A B) f a))))).
tt('thm/finite_map/FUPDATE_COMMUTES_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), a : A, b : B, c : A, d : B]: ((~ (a = c)) => ((('const/finite_map/FUPDATE' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a b)) (('const/pair/,' A B) c d)) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) c d)) (('const/pair/,' A B) a b)))))).
tt('thm/finite_map/FUPDATE_EQ_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), a : A, b : B, c : B]: ((('const/finite_map/FUPDATE' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a b)) (('const/pair/,' A B) a c)) = (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a c))))).
tt('thm/finite_map/FDOM_FEMPTY_', ax, ![A : $t, B : $t]: ((('const/finite_map/FDOM' A B) ('const/finite_map/FEMPTY' A B)) = ('const/pred_set/EMPTY' A))).
tt('thm/finite_map/FDOM_FUPDATE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), a : A, b : B]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a b))) = (('const/pred_set/INSERT' A) a (('const/finite_map/FDOM' A B) f))))).
tt('thm/finite_map/FAPPLY_FUPDATE_THM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), a : A, b : B, x : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a b)) x) = (('const/bool/COND' B) (x = a) b (('const/finite_map/FAPPLY' A B) f x))))).
tt('thm/finite_map/NOT_EQ_FEMPTY_FUPDATE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), a : A, b : B]: (~ (('const/finite_map/FEMPTY' A B) = (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) a b)))))).
tt('thm/finite_map/FDOM_EQ_FDOM_FUPDATE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) => (![y : B]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))) = (('const/finite_map/FDOM' A B) f)))))).
tt('thm/finite_map/fmap_SIMPLE_INDUCT_', ax, ![A : $t, B : $t]: (![P : (('type/finite_map/fmap' A B) > $o)]: (((P ('const/finite_map/FEMPTY' A B)) & (![f : ('type/finite_map/fmap' A B)]: ((P f) => (![x : A, y : B]: (P (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))))))) => (![f : ('type/finite_map/fmap' A B)]: (P f))))).
tt('thm/finite_map/FDOM_EQ_EMPTY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FDOM' A B) f) = ('const/pred_set/EMPTY' A)) = (f = ('const/finite_map/FEMPTY' A B))))).
tt('thm/finite_map/FDOM_EQ_EMPTY_SYM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/pred_set/EMPTY' A) = (('const/finite_map/FDOM' A B) f)) = (f = ('const/finite_map/FEMPTY' A B))))).
tt('thm/finite_map/FDOM_F_FEMPTY1_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((![a : A]: (~ (('const/bool/IN' A) a (('const/finite_map/FDOM' A B) f)))) = (f = ('const/finite_map/FEMPTY' A B))))).
tt('thm/finite_map/FDOM_FINITE_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B)]: (('const/pred_set/FINITE' A) (('const/finite_map/FDOM' A B) fm)))).
tt('thm/finite_map/FCARD_DEF_', def, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FCARD' A B) fm) = (('const/pred_set/CARD' A) (('const/finite_map/FDOM' A B) fm))))).
tt('thm/finite_map/FCARD_FEMPTY_', ax, ![A : $t, B : $t]: ((('const/finite_map/FCARD' A B) ('const/finite_map/FEMPTY' A B)) = 'const/num/0')).
tt('thm/finite_map/FCARD_FUPDATE_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), a : A, b : B]: ((('const/finite_map/FCARD' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) a b))) = (('const/bool/COND' 'type/num/num') (('const/bool/IN' A) a (('const/finite_map/FDOM' A B) fm)) (('const/finite_map/FCARD' A B) fm) ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/finite_map/FCARD' A B) fm)))))).
tt('thm/finite_map/FCARD_0_FEMPTY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FCARD' A B) f) = 'const/num/0') = (f = ('const/finite_map/FEMPTY' A B))))).
tt('thm/finite_map/FCARD_SUC_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), n : 'type/num/num']: (((('const/finite_map/FCARD' A B) f) = ('const/num/SUC' n)) = (?['f\'' : ('type/finite_map/fmap' A B), x : A, y : B]: ((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) 'f\''))) & (((('const/finite_map/FCARD' A B) 'f\'') = n) & (f = (('const/finite_map/FUPDATE' A B) 'f\'' (('const/pair/,' A B) x y))))))))).
tt('thm/finite_map/fmap_INDUCT_', ax, ![A : $t, B : $t]: (![P : (('type/finite_map/fmap' A B) > $o)]: (((P ('const/finite_map/FEMPTY' A B)) & (![f : ('type/finite_map/fmap' A B)]: ((P f) => (![x : A, y : B]: ((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f))) => (P (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)))))))) => (![f : ('type/finite_map/fmap' A B)]: (P f))))).
tt('thm/finite_map/FM_PULL_APART_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A]: ((('const/bool/IN' A) k (('const/finite_map/FDOM' A B) fm)) => (?[fm0 : ('type/finite_map/fmap' A B), v : B]: ((fm = (('const/finite_map/FUPDATE' A B) fm0 (('const/pair/,' A B) k v))) & (~ (('const/bool/IN' A) k (('const/finite_map/FDOM' A B) fm0)))))))).
tt('thm/finite_map/NOT_FDOM_FAPPLY_FEMPTY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f))) => ((('const/finite_map/FAPPLY' A B) f x) = (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) x))))).
tt('thm/finite_map/fmap_EQ_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((((('const/finite_map/FDOM' A B) f) = (('const/finite_map/FDOM' A B) g)) & ((('const/finite_map/FAPPLY' A B) f) = (('const/finite_map/FAPPLY' A B) g))) = (f = g)))).
tt('thm/finite_map/fmap_EQ_THM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((((('const/finite_map/FDOM' A B) f) = (('const/finite_map/FDOM' A B) g)) & (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) => ((('const/finite_map/FAPPLY' A B) f x) = (('const/finite_map/FAPPLY' A B) g x))))) = (f = g)))).
tt('thm/finite_map/fmap_EXT_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((f = g) = (((('const/finite_map/FDOM' A B) f) = (('const/finite_map/FDOM' A B) g)) & (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) => ((('const/finite_map/FAPPLY' A B) f x) = (('const/finite_map/FAPPLY' A B) g x)))))))).
tt('thm/finite_map/SUBMAP_DEF_', def, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) f g) = (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) => ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) g)) & ((('const/finite_map/FAPPLY' A B) f x) = (('const/finite_map/FAPPLY' A B) g x)))))))).
tt('thm/finite_map/SUBMAP_FEMPTY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: (('const/finite_map/SUBMAP' A B) ('const/finite_map/FEMPTY' A B) f))).
tt('thm/finite_map/SUBMAP_REFL_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: (('const/finite_map/SUBMAP' A B) f f))).
tt('thm/finite_map/SUBMAP_ANTISYM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: (((('const/finite_map/SUBMAP' A B) f g) & (('const/finite_map/SUBMAP' A B) g f)) = (f = g)))).
tt('thm/finite_map/SUBMAP_TRANS_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), h : ('type/finite_map/fmap' A B)]: (((('const/finite_map/SUBMAP' A B) f g) & (('const/finite_map/SUBMAP' A B) g h)) => (('const/finite_map/SUBMAP' A B) f h)))).
tt('thm/finite_map/EQ_FDOM_SUBMAP_', ax, ![A : $t, B : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: ((f = g) = ((('const/finite_map/SUBMAP' A B) f g) & ((('const/finite_map/FDOM' A B) f) = (('const/finite_map/FDOM' A B) g)))))).
tt('thm/finite_map/SUBMAP_FUPDATE_EQN_', ax, ![A : $t, B : $t]: (![y : B, x : A, f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) f (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))) = ((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f))) | (((('const/finite_map/FAPPLY' A B) f x) = y) & (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f))))))).
tt('thm/finite_map/DRESTRICT_DEF_0', def, ![A : $t, B : $t]: (![r : (A > $o), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/DRESTRICT' A B) f r)) = (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f) r)))).
tt('thm/finite_map/DRESTRICT_DEF_e1', def, ![A : $t, B : $t]: (![r : (A > $o), f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/DRESTRICT' A B) f r) x) = (('const/bool/COND' B) (('const/bool/IN' A) x (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f) r)) (('const/finite_map/FAPPLY' A B) f x) (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) x))))).
tt('thm/finite_map/DRESTRICT_FEMPTY_', ax, ![A : $t, B : $t]: (![r : (A > $o)]: ((('const/finite_map/DRESTRICT' A B) ('const/finite_map/FEMPTY' A B) r) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/DRESTRICT_FUPDATE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), r : (A > $o), x : A, y : B]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) r) = (('const/bool/COND' ('type/finite_map/fmap' A B)) (('const/bool/IN' A) x r) (('const/finite_map/FUPDATE' A B) (('const/finite_map/DRESTRICT' A B) f r) (('const/pair/,' A B) x y)) (('const/finite_map/DRESTRICT' A B) f r))))).
tt('thm/finite_map/STRONG_DRESTRICT_FUPDATE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), r : (A > $o), x : A, y : B]: ((('const/bool/IN' A) x r) => ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) r) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/DELETE' A) r x)) (('const/pair/,' A B) x y)))))).
tt('thm/finite_map/FDOM_DRESTRICT_', ax, ![A : $t, B : $t, C : $t]: (![f : ('type/finite_map/fmap' A B), r : (A > $o), x : C]: ((('const/finite_map/FDOM' A B) (('const/finite_map/DRESTRICT' A B) f r)) = (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f) r)))).
tt('thm/finite_map/NOT_FDOM_DRESTRICT_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f))) => ((('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))) = f)))).
tt('thm/finite_map/DRESTRICT_SUBMAP_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), r : (A > $o)]: (('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f r) f))).
tt('thm/finite_map/DRESTRICT_DRESTRICT_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), P : (A > $o), Q : (A > $o)]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/DRESTRICT' A B) f P) Q) = (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/INTER' A) P Q))))).
tt('thm/finite_map/DRESTRICT_IS_FEMPTY_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/DRESTRICT' A B) f ('const/pred_set/EMPTY' A)) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FUPDATE_DRESTRICT_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))) (('const/pair/,' A B) x y))))).
tt('thm/finite_map/STRONG_DRESTRICT_FUPDATE_THM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), r : (A > $o), x : A, y : B]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) r) = (('const/bool/COND' ('type/finite_map/fmap' A B)) (('const/bool/IN' A) x r) (('const/finite_map/FUPDATE' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) r)) (('const/pair/,' A B) x y)) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/INTER' A) (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))) r)))))).
tt('thm/finite_map/DRESTRICT_UNIV_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/DRESTRICT' A B) f ('const/pred_set/UNIV' A)) = f))).
tt('thm/finite_map/SUBMAP_DRESTRICT_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), P : (A > $o)]: (('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f P) f))).
tt('thm/finite_map/DRESTRICT_EQ_DRESTRICT_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), s1 : (A > $o), s2 : (A > $o)]: (((('const/finite_map/DRESTRICT' A B) f1 s1) = (('const/finite_map/DRESTRICT' A B) f2 s2)) = ((('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f1 s1) f2) & ((('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f2 s2) f1) & ((('const/pred_set/INTER' A) s1 (('const/finite_map/FDOM' A B) f1)) = (('const/pred_set/INTER' A) s2 (('const/finite_map/FDOM' A B) f2)))))))).
tt('thm/finite_map/FUNION_DEF_0', def, ![A : $t, B : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUNION' A B) f g)) = (('const/pred_set/UNION' A) (('const/finite_map/FDOM' A B) f) (('const/finite_map/FDOM' A B) g))))).
tt('thm/finite_map/FUNION_DEF_e1', def, ![A : $t, B : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUNION' A B) f g) x) = (('const/bool/COND' B) (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) (('const/finite_map/FAPPLY' A B) f x) (('const/finite_map/FAPPLY' A B) g x))))).
tt('thm/finite_map/FUNION_FEMPTY_1_', ax, ![A : $t, B : $t]: (![g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) ('const/finite_map/FEMPTY' A B) g) = g))).
tt('thm/finite_map/FUNION_FEMPTY_2_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) f ('const/finite_map/FEMPTY' A B)) = f))).
tt('thm/finite_map/FUNION_FUPDATE_1_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FUNION' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) g) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/FUNION' A B) f g) (('const/pair/,' A B) x y))))).
tt('thm/finite_map/FUNION_FUPDATE_2_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FUNION' A B) f (('const/finite_map/FUPDATE' A B) g (('const/pair/,' A B) x y))) = (('const/bool/COND' ('type/finite_map/fmap' A B)) (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) (('const/finite_map/FUNION' A B) f g) (('const/finite_map/FUPDATE' A B) (('const/finite_map/FUNION' A B) f g) (('const/pair/,' A B) x y)))))).
tt('thm/finite_map/FDOM_FUNION_', ax, ![A : $t, B : $t, C : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : C]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUNION' A B) f g)) = (('const/pred_set/UNION' A) (('const/finite_map/FDOM' A B) f) (('const/finite_map/FDOM' A B) g))))).
tt('thm/finite_map/FUNION_IDEMPOT_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) fm fm) = fm))).
tt('thm/finite_map/FMERGE_DEF_0', def, ![B : $t, A : $t]: (![m : (A > (A > A)), g : ('type/finite_map/fmap' B A), f : ('type/finite_map/fmap' B A)]: ((('const/finite_map/FDOM' B A) (('const/finite_map/FMERGE' A B) m f g)) = (('const/pred_set/UNION' B) (('const/finite_map/FDOM' B A) f) (('const/finite_map/FDOM' B A) g))))).
tt('thm/finite_map/FMERGE_DEF_e1', def, ![B : $t, A : $t]: (![m : (A > (A > A)), g : ('type/finite_map/fmap' B A), f : ('type/finite_map/fmap' B A), x : B]: ((('const/finite_map/FAPPLY' B A) (('const/finite_map/FMERGE' A B) m f g) x) = (('const/bool/COND' A) (~ (('const/bool/IN' B) x (('const/finite_map/FDOM' B A) f))) (('const/finite_map/FAPPLY' B A) g x) (('const/bool/COND' A) (~ (('const/bool/IN' B) x (('const/finite_map/FDOM' B A) g))) (('const/finite_map/FAPPLY' B A) f x) (m (('const/finite_map/FAPPLY' B A) f x) (('const/finite_map/FAPPLY' B A) g x))))))).
tt('thm/finite_map/FMERGE_FEMPTY_0', ax, ![A : $t, B : $t]: (![m : (B > (B > B)), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FMERGE' B A) m f ('const/finite_map/FEMPTY' A B)) = f))).
tt('thm/finite_map/FMERGE_FEMPTY_e1', ax, ![A : $t, B : $t]: (![m : (B > (B > B)), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FMERGE' B A) m ('const/finite_map/FEMPTY' A B) f) = f))).
tt('thm/finite_map/FDOM_FMERGE_', ax, ![B : $t, A : $t]: (![m : (A > (A > A)), f : ('type/finite_map/fmap' B A), g : ('type/finite_map/fmap' B A)]: ((('const/finite_map/FDOM' B A) (('const/finite_map/FMERGE' A B) m f g)) = (('const/pred_set/UNION' B) (('const/finite_map/FDOM' B A) f) (('const/finite_map/FDOM' B A) g))))).
tt('thm/finite_map/FMERGE_FUNION_', ax, ![B : $t, A : $t]: (('const/finite_map/FUNION' A B) = (('const/finite_map/FMERGE' B A) (^[x : B, y : B]: x)))).
tt('thm/finite_map/FUNION_FMERGE_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), m : (B > (B > B))]: ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f2)) => ((('const/finite_map/FMERGE' B A) m f1 f2) = (('const/finite_map/FUNION' A B) f1 f2))))).
tt('thm/finite_map/FMERGE_NO_CHANGE_0', ax, ![A : $t, B : $t]: (![m : (B > (B > B)), f2 : ('type/finite_map/fmap' A B), f1 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FMERGE' B A) m f1 f2) = f1) = (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f2)) => ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f1)) & ((m (('const/finite_map/FAPPLY' A B) f1 x) (('const/finite_map/FAPPLY' A B) f2 x)) = (('const/finite_map/FAPPLY' A B) f1 x)))))))).
tt('thm/finite_map/FMERGE_NO_CHANGE_e1', ax, ![A : $t, B : $t]: (![m : (B > (B > B)), f2 : ('type/finite_map/fmap' A B), f1 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FMERGE' B A) m f1 f2) = f2) = (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f1)) => ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f2)) & ((m (('const/finite_map/FAPPLY' A B) f1 x) (('const/finite_map/FAPPLY' A B) f2 x)) = (('const/finite_map/FAPPLY' A B) f2 x)))))))).
tt('thm/finite_map/FMERGE_COMM_', ax, ![B : $t, A : $t]: (![m : (B > (B > B))]: ((('const/operator/COMM' ('type/finite_map/fmap' A B) ('type/finite_map/fmap' A B)) (('const/finite_map/FMERGE' B A) m)) = (('const/operator/COMM' B B) m)))).
tt('thm/finite_map/FMERGE_ASSOC_', ax, ![B : $t, A : $t]: (![m : (B > (B > B))]: ((('const/operator/ASSOC' ('type/finite_map/fmap' A B)) (('const/finite_map/FMERGE' B A) m)) = (('const/operator/ASSOC' B) m)))).
tt('thm/finite_map/FMERGE_DRESTRICT_', ax, ![A : $t, B : $t]: (![vs : (A > $o), st2 : ('type/finite_map/fmap' A B), st1 : ('type/finite_map/fmap' A B), f : (B > (B > B))]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/FMERGE' B A) f st1 st2) vs) = (('const/finite_map/FMERGE' B A) f (('const/finite_map/DRESTRICT' A B) st1 vs) (('const/finite_map/DRESTRICT' A B) st2 vs))))).
tt('thm/finite_map/FMERGE_EQ_FEMPTY_', ax, ![A : $t, B : $t]: (![m : (B > (B > B)), g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FMERGE' B A) m f g) = ('const/finite_map/FEMPTY' A B)) = ((f = ('const/finite_map/FEMPTY' A B)) & (g = ('const/finite_map/FEMPTY' A B)))))).
tt('thm/finite_map/FLOOKUP_DEF_', def, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FLOOKUP' A B) f x) = (('const/bool/COND' ('type/option/option' B)) (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) (('const/option/SOME' B) (('const/finite_map/FAPPLY' A B) f x)) ('const/option/NONE' B))))).
tt('thm/finite_map/FLOOKUP_EMPTY_', ax, ![A : $t, B : $t]: (![k : B]: ((('const/finite_map/FLOOKUP' B A) ('const/finite_map/FEMPTY' B A) k) = ('const/option/NONE' A)))).
tt('thm/finite_map/FLOOKUP_UPDATE_', ax, ![B : $t, A : $t]: (![v : A, k2 : B, k1 : B, fm : ('type/finite_map/fmap' B A)]: ((('const/finite_map/FLOOKUP' B A) (('const/finite_map/FUPDATE' B A) fm (('const/pair/,' B A) k1 v)) k2) = (('const/bool/COND' ('type/option/option' A)) (k1 = k2) (('const/option/SOME' A) v) (('const/finite_map/FLOOKUP' B A) fm k2))))).
tt('thm/finite_map/FLOOKUP_SUBMAP_', ax, ![B : $t, A : $t]: (![v : B, k : A, g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/SUBMAP' A B) f g) & ((('const/finite_map/FLOOKUP' A B) f k) = (('const/option/SOME' B) v))) => ((('const/finite_map/FLOOKUP' A B) g k) = (('const/option/SOME' B) v))))).
tt('thm/finite_map/SUBMAP_FUPDATE_FLOOKUP_', ax, ![B : $t, A : $t]: (![y : B, x : A, f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) f (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))) = (((('const/finite_map/FLOOKUP' A B) f x) = ('const/option/NONE' B)) | ((('const/finite_map/FLOOKUP' A B) f x) = (('const/option/SOME' B) y)))))).
tt('thm/finite_map/FLOOKUP_FUNION_', ax, ![A : $t, B : $t]: (![k : B, f2 : ('type/finite_map/fmap' B A), f1 : ('type/finite_map/fmap' B A)]: ((('const/finite_map/FLOOKUP' B A) (('const/finite_map/FUNION' B A) f1 f2) k) = (('const/option/option_CASE' A ('type/option/option' A)) (('const/finite_map/FLOOKUP' B A) f1 k) (('const/finite_map/FLOOKUP' B A) f2 k) (^[v : A]: (('const/option/SOME' A) v)))))).
tt('thm/finite_map/FLOOKUP_EXT_', ax, ![A : $t, B : $t]: (![f2 : ('type/finite_map/fmap' A B), f1 : ('type/finite_map/fmap' A B)]: ((f1 = f2) = ((('const/finite_map/FLOOKUP' A B) f1) = (('const/finite_map/FLOOKUP' A B) f2))))).
tt('thm/finite_map/FEVERY_DEF_', def, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > $o), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FEVERY' A B) P f) = (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) => (P (('const/pair/,' A B) x (('const/finite_map/FAPPLY' A B) f x)))))))).
tt('thm/finite_map/FEVERY_FEMPTY_', ax, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > $o)]: (('const/finite_map/FEVERY' A B) P ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FEVERY_FUPDATE_', ax, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > $o), f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FEVERY' A B) P (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))) = ((P (('const/pair/,' A B) x y)) & (('const/finite_map/FEVERY' A B) P (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))))).
tt('thm/finite_map/FEVERY_FLOOKUP_', ax, ![B : $t, A : $t]: (![v : B, k : A, f : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A B) > $o)]: (((('const/finite_map/FEVERY' A B) P f) & ((('const/finite_map/FLOOKUP' A B) f k) = (('const/option/SOME' B) v))) => (P (('const/pair/,' A B) k v))))).
tt('thm/finite_map/f_o_f_DEF_0', def, ![B : $t, C : $t, A : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' B C)]: ((('const/finite_map/FDOM' A C) (('const/finite_map/f_o_f' A B C) f g)) = (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) g) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (('const/finite_map/FAPPLY' A B) g x) (('const/finite_map/FDOM' B C) f))))))))).
tt('thm/finite_map/f_o_f_DEF_e1', def, ![A : $t, B : $t, C : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' B C), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) (('const/finite_map/f_o_f' A B C) f g))) => ((('const/finite_map/FAPPLY' A C) (('const/finite_map/f_o_f' A B C) f g) x) = (('const/finite_map/FAPPLY' B C) f (('const/finite_map/FAPPLY' A B) g x)))))).
tt('thm/finite_map/f_o_f_FEMPTY_1_', ax, ![A : $t, C : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/f_o_f' A B C) ('const/finite_map/FEMPTY' B C) f) = ('const/finite_map/FEMPTY' A C)))).
tt('thm/finite_map/f_o_f_FEMPTY_2_', ax, ![A : $t, C : $t, B : $t]: (![f : ('type/finite_map/fmap' B C)]: ((('const/finite_map/f_o_f' A B C) f ('const/finite_map/FEMPTY' A B)) = ('const/finite_map/FEMPTY' A C)))).
tt('thm/finite_map/o_f_DEF_0', def, ![A : $t, B : $t, C : $t]: (![g : ('type/finite_map/fmap' A B), f : (B > C)]: ((('const/finite_map/FDOM' A C) (('const/finite_map/o_f' A B C) f g)) = (('const/finite_map/FDOM' A B) g)))).
tt('thm/finite_map/o_f_DEF_e1', def, ![A : $t, B : $t, C : $t]: (![g : ('type/finite_map/fmap' A B), f : (B > C), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) (('const/finite_map/o_f' A B C) f g))) => ((('const/finite_map/FAPPLY' A C) (('const/finite_map/o_f' A B C) f g) x) = (f (('const/finite_map/FAPPLY' A B) g x)))))).
tt('thm/finite_map/o_f_FDOM_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) g) = (('const/finite_map/FDOM' A C) (('const/finite_map/o_f' A B C) f g))))).
tt('thm/finite_map/FDOM_o_f_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A C) (('const/finite_map/o_f' A B C) f g)) = (('const/finite_map/FDOM' A B) g)))).
tt('thm/finite_map/o_f_FAPPLY_', ax, ![A : $t, B : $t, C : $t]: (![f : (B > C), g : ('type/finite_map/fmap' A B), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) g)) => ((('const/finite_map/FAPPLY' A C) (('const/finite_map/o_f' A B C) f g) x) = (f (('const/finite_map/FAPPLY' A B) g x)))))).
tt('thm/finite_map/o_f_FEMPTY_', ax, ![A : $t, B : $t, C : $t]: (![f : (C > B)]: ((('const/finite_map/o_f' A C B) f ('const/finite_map/FEMPTY' A C)) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FEVERY_o_f_', ax, ![A : $t, B : $t, C : $t]: (![m : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A C) > $o), f : (B > C)]: ((('const/finite_map/FEVERY' A C) P (('const/finite_map/o_f' A B C) f m)) = (('const/finite_map/FEVERY' A B) (^[x : ('type/pair/prod' A B)]: (P (('const/pair/,' A C) (('const/pair/FST' A B) x) (f (('const/pair/SND' A B) x))))) m)))).
tt('thm/finite_map/o_f_o_f_', ax, ![A : $t, D : $t, C : $t, B : $t]: (![h : ('type/finite_map/fmap' A D), g : (D > C), f : (C > B)]: ((('const/finite_map/o_f' A C B) f (('const/finite_map/o_f' A D C) g h)) = (('const/finite_map/o_f' A D B) (('const/combin/o' D B C) f g) h)))).
tt('thm/finite_map/FLOOKUP_o_f_', ax, ![C : $t, A : $t, B : $t]: (![k : B, fm : ('type/finite_map/fmap' B C), f : (C > A)]: ((('const/finite_map/FLOOKUP' B A) (('const/finite_map/o_f' B C A) f fm) k) = (('const/option/option_CASE' C ('type/option/option' A)) (('const/finite_map/FLOOKUP' B C) fm k) ('const/option/NONE' A) (^[v : C]: (('const/option/SOME' A) (f v))))))).
tt('thm/finite_map/FRANGE_DEF_', def, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FRANGE' A B) f) = (('const/pred_set/GSPEC' B B) (^[y : B]: (('const/pair/,' B $o) y (?[x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) & ((('const/finite_map/FAPPLY' A B) f x) = y))))))))).
tt('thm/finite_map/FRANGE_FEMPTY_', ax, ![A : $t, B : $t]: ((('const/finite_map/FRANGE' B A) ('const/finite_map/FEMPTY' B A)) = ('const/pred_set/EMPTY' A))).
tt('thm/finite_map/FRANGE_FUPDATE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FRANGE' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y))) = (('const/pred_set/INSERT' B) y (('const/finite_map/FRANGE' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A))))))))).
tt('thm/finite_map/SUBMAP_FRANGE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) f g) => (('const/pred_set/SUBSET' B) (('const/finite_map/FRANGE' A B) f) (('const/finite_map/FRANGE' A B) g))))).
tt('thm/finite_map/FINITE_FRANGE_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B)]: (('const/pred_set/FINITE' B) (('const/finite_map/FRANGE' A B) fm)))).
tt('thm/finite_map/o_f_FRANGE_', ax, ![B : $t, A : $t, C : $t]: (![x : A, g : ('type/finite_map/fmap' B A), f : (A > C)]: ((('const/bool/IN' A) x (('const/finite_map/FRANGE' B A) g)) => (('const/bool/IN' C) (f x) (('const/finite_map/FRANGE' B C) (('const/finite_map/o_f' B A C) f g)))))).
tt('thm/finite_map/FRANGE_FLOOKUP_', ax, ![A : $t, B : $t]: (![v : A, f : ('type/finite_map/fmap' B A)]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) f)) = (?[k : B]: ((('const/finite_map/FLOOKUP' B A) f k) = (('const/option/SOME' A) v)))))).
tt('thm/finite_map/FRANGE_FUNION_', ax, ![A : $t, B : $t]: (![fm2 : ('type/finite_map/fmap' A B), fm1 : ('type/finite_map/fmap' A B)]: ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) fm1) (('const/finite_map/FDOM' A B) fm2)) => ((('const/finite_map/FRANGE' A B) (('const/finite_map/FUNION' A B) fm1 fm2)) = (('const/pred_set/UNION' B) (('const/finite_map/FRANGE' A B) fm1) (('const/finite_map/FRANGE' A B) fm2)))))).
tt('thm/finite_map/RRESTRICT_DEF_0', def, ![B : $t, A : $t]: (![r : (B > $o), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/RRESTRICT' A B) f r)) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) & (('const/bool/IN' B) (('const/finite_map/FAPPLY' A B) f x) r)))))))).
tt('thm/finite_map/RRESTRICT_DEF_e1', def, ![A : $t, B : $t]: (![r : (B > $o), f : ('type/finite_map/fmap' A B), x : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/RRESTRICT' A B) f r) x) = (('const/bool/COND' B) ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) & (('const/bool/IN' B) (('const/finite_map/FAPPLY' A B) f x) r)) (('const/finite_map/FAPPLY' A B) f x) (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) x))))).
tt('thm/finite_map/RRESTRICT_FEMPTY_', ax, ![B : $t, A : $t]: (![r : (A > $o)]: ((('const/finite_map/RRESTRICT' B A) ('const/finite_map/FEMPTY' B A) r) = ('const/finite_map/FEMPTY' B A)))).
tt('thm/finite_map/RRESTRICT_FUPDATE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), r : (B > $o), x : A, y : B]: ((('const/finite_map/RRESTRICT' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) r) = (('const/bool/COND' ('type/finite_map/fmap' A B)) (('const/bool/IN' B) y r) (('const/finite_map/FUPDATE' A B) (('const/finite_map/RRESTRICT' A B) f r) (('const/pair/,' A B) x y)) (('const/finite_map/RRESTRICT' A B) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) x ('const/pred_set/EMPTY' A)))) r))))).
tt('thm/finite_map/FUN_FMAP_DEF_', def, ![A : $t, B : $t]: (![f : (A > B), P : (A > $o)]: ((('const/pred_set/FINITE' A) P) => (((('const/finite_map/FDOM' A B) (('const/finite_map/FUN_FMAP' A B) f P)) = P) & (![x : A]: ((('const/bool/IN' A) x P) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUN_FMAP' A B) f P) x) = (f x)))))))).
tt('thm/finite_map/FUN_FMAP_EMPTY_', ax, ![A : $t, B : $t]: (![f : (A > B)]: ((('const/finite_map/FUN_FMAP' A B) f ('const/pred_set/EMPTY' A)) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FRANGE_FMAP_', ax, ![A : $t, B : $t]: (![f : (A > B), P : (A > $o)]: ((('const/pred_set/FINITE' A) P) => ((('const/finite_map/FRANGE' A B) (('const/finite_map/FUN_FMAP' A B) f P)) = (('const/pred_set/IMAGE' A B) f P))))).
tt('thm/finite_map/FDOM_FMAP_', ax, ![A : $t, B : $t]: (![f : (A > B), s : (A > $o)]: ((('const/pred_set/FINITE' A) s) => ((('const/finite_map/FDOM' A B) (('const/finite_map/FUN_FMAP' A B) f s)) = s)))).
tt('thm/finite_map/FLOOKUP_FUN_FMAP_', ax, ![B : $t, A : $t]: (![k : A, f : (A > B), P : (A > $o)]: ((('const/pred_set/FINITE' A) P) => ((('const/finite_map/FLOOKUP' A B) (('const/finite_map/FUN_FMAP' A B) f P) k) = (('const/bool/COND' ('type/option/option' B)) (('const/bool/IN' A) k P) (('const/option/SOME' B) (f k)) ('const/option/NONE' B)))))).
tt('thm/finite_map/f_o_DEF_', def, ![B : $t, C : $t, A : $t]: (![f : ('type/finite_map/fmap' B C), g : (A > B)]: ((('const/finite_map/f_o' A B C) f g) = (('const/finite_map/f_o_f' A B C) f (('const/finite_map/FUN_FMAP' A B) g (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (g x) (('const/finite_map/FDOM' B C) f)))))))))).
tt('thm/finite_map/FDOM_f_o_', ax, ![B : $t, C : $t, A : $t]: (![f : ('type/finite_map/fmap' B C), g : (A > B)]: ((('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (g x) (('const/finite_map/FDOM' B C) f)))))) => ((('const/finite_map/FDOM' A C) (('const/finite_map/f_o' A B C) f g)) = (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (g x) (('const/finite_map/FDOM' B C) f))))))))).
tt('thm/finite_map/f_o_FEMPTY_', ax, ![A : $t, C : $t, B : $t]: (![g : (A > B)]: ((('const/finite_map/f_o' A B C) ('const/finite_map/FEMPTY' B C) g) = ('const/finite_map/FEMPTY' A C)))).
tt('thm/finite_map/f_o_FUPDATE_', ax, ![A : $t, C : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A, v : B, g : (C > A)]: (((('const/pred_set/FINITE' C) (('const/pred_set/GSPEC' C C) (^[x : C]: (('const/pair/,' C $o) x (('const/bool/IN' A) (g x) (('const/finite_map/FDOM' A B) fm)))))) & (('const/pred_set/FINITE' C) (('const/pred_set/GSPEC' C C) (^[x : C]: (('const/pair/,' C $o) x ((g x) = k)))))) => ((('const/finite_map/f_o' C A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) g) = (('const/finite_map/FMERGE' B C) (('const/combin/C' B B B) ('const/combin/K' B B)) (('const/finite_map/f_o' C A B) fm g) (('const/finite_map/FUN_FMAP' C B) (('const/combin/K' B C) v) (('const/pred_set/GSPEC' C C) (^[x : C]: (('const/pair/,' C $o) x ((g x) = k)))))))))).
tt('thm/finite_map/FAPPLY_f_o_', ax, ![A : $t, B : $t, C : $t]: (![f : ('type/finite_map/fmap' B C), g : (A > B)]: ((('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (g x) (('const/finite_map/FDOM' B C) f)))))) => (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) (('const/finite_map/f_o' A B C) f g))) => ((('const/finite_map/FAPPLY' A C) (('const/finite_map/f_o' A B C) f g) x) = (('const/finite_map/FAPPLY' B C) f (g x)))))))).
tt('thm/finite_map/FINITE_PRED_11_', ax, ![B : $t, C : $t, A : $t]: (![g : (A > B)]: ((![x : A, y : A]: (((g x) = (g y)) = (x = y))) => (![f : ('type/finite_map/fmap' B C)]: (('const/pred_set/FINITE' A) (('const/pred_set/GSPEC' A A) (^[x : A]: (('const/pair/,' A $o) x (('const/bool/IN' B) (g x) (('const/finite_map/FDOM' B C) f)))))))))).
tt('thm/finite_map/fmap_domsub_', def, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A]: ((('const/finite_map/fdomsub' A B) fm k) = (('const/finite_map/DRESTRICT' A B) fm (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) k ('const/pred_set/EMPTY' A))))))).
tt('thm/finite_map/DOMSUB_FEMPTY_', ax, ![A : $t, B : $t]: (![k : A]: ((('const/finite_map/fdomsub' A B) ('const/finite_map/FEMPTY' A B) k) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/DOMSUB_FUPDATE_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A, v : B]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) k) = (('const/finite_map/fdomsub' A B) fm k)))).
tt('thm/finite_map/DOMSUB_FUPDATE_NEQ_', ax, ![B : $t, A : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A, v : B]: ((~ (k1 = k2)) => ((('const/finite_map/fdomsub' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k1 v)) k2) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/fdomsub' A B) fm k2) (('const/pair/,' A B) k1 v)))))).
tt('thm/finite_map/DOMSUB_FUPDATE_THM_', ax, ![B : $t, A : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A, v : B]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k1 v)) k2) = (('const/bool/COND' ('type/finite_map/fmap' A B)) (k1 = k2) (('const/finite_map/fdomsub' A B) fm k2) (('const/finite_map/FUPDATE' A B) (('const/finite_map/fdomsub' A B) fm k2) (('const/pair/,' A B) k1 v)))))).
tt('thm/finite_map/FDOM_DOMSUB_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A]: ((('const/finite_map/FDOM' A B) (('const/finite_map/fdomsub' A B) fm k)) = (('const/pred_set/DELETE' A) (('const/finite_map/FDOM' A B) fm) k)))).
tt('thm/finite_map/DOMSUB_FAPPLY_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/fdomsub' A B) fm k) k) = (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) k)))).
tt('thm/finite_map/DOMSUB_FAPPLY_NEQ_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A]: ((~ (k1 = k2)) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/fdomsub' A B) fm k1) k2) = (('const/finite_map/FAPPLY' A B) fm k2))))).
tt('thm/finite_map/DOMSUB_FAPPLY_THM_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A]: ((('const/finite_map/FAPPLY' A B) (('const/finite_map/fdomsub' A B) fm k1) k2) = (('const/bool/COND' B) (k1 = k2) (('const/finite_map/FAPPLY' A B) ('const/finite_map/FEMPTY' A B) k2) (('const/finite_map/FAPPLY' A B) fm k2))))).
tt('thm/finite_map/DOMSUB_FLOOKUP_', ax, ![B : $t, A : $t]: (![fm : ('type/finite_map/fmap' A B), k : A]: ((('const/finite_map/FLOOKUP' A B) (('const/finite_map/fdomsub' A B) fm k) k) = ('const/option/NONE' B)))).
tt('thm/finite_map/DOMSUB_FLOOKUP_NEQ_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A]: ((~ (k1 = k2)) => ((('const/finite_map/FLOOKUP' A B) (('const/finite_map/fdomsub' A B) fm k1) k2) = (('const/finite_map/FLOOKUP' A B) fm k2))))).
tt('thm/finite_map/DOMSUB_FLOOKUP_THM_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k1 : A, k2 : A]: ((('const/finite_map/FLOOKUP' A B) (('const/finite_map/fdomsub' A B) fm k1) k2) = (('const/bool/COND' ('type/option/option' B)) (k1 = k2) ('const/option/NONE' B) (('const/finite_map/FLOOKUP' A B) fm k2))))).
tt('thm/finite_map/FRANGE_FUPDATE_DOMSUB_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), k : A, v : B]: ((('const/finite_map/FRANGE' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v))) = (('const/pred_set/INSERT' B) v (('const/finite_map/FRANGE' A B) (('const/finite_map/fdomsub' A B) fm k)))))).
tt('thm/finite_map/o_f_DOMSUB_', ax, ![A : $t, C : $t, B : $t]: (![k : A, g : (C > B), fm : ('type/finite_map/fmap' A C)]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/o_f' A C B) g fm) k) = (('const/finite_map/o_f' A C B) g (('const/finite_map/fdomsub' A C) fm k))))).
tt('thm/finite_map/DOMSUB_IDEM_', ax, ![A : $t, B : $t]: (![k : A, fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/fdomsub' A B) fm k) k) = (('const/finite_map/fdomsub' A B) fm k)))).
tt('thm/finite_map/DOMSUB_COMMUTES_', ax, ![A : $t, B : $t]: (![k2 : A, k1 : A, fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/fdomsub' A B) fm k1) k2) = (('const/finite_map/fdomsub' A B) (('const/finite_map/fdomsub' A B) fm k2) k1)))).
tt('thm/finite_map/o_f_FUPDATE_', ax, ![C : $t, B : $t, A : $t]: (![v : C, k : A, fm : ('type/finite_map/fmap' A C), f : (C > B)]: ((('const/finite_map/o_f' A C B) f (('const/finite_map/FUPDATE' A C) fm (('const/pair/,' A C) k v))) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/o_f' A C B) f (('const/finite_map/fdomsub' A C) fm k)) (('const/pair/,' A B) k (f v)))))).
tt('thm/finite_map/DOMSUB_NOT_IN_DOM_', ax, ![A : $t, B : $t]: (![k : A, fm : ('type/finite_map/fmap' A B)]: ((~ (('const/bool/IN' A) k (('const/finite_map/FDOM' A B) fm))) => ((('const/finite_map/fdomsub' A B) fm k) = fm)))).
tt('thm/finite_map/fmap_CASES_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B)]: ((f = ('const/finite_map/FEMPTY' A B)) | (?[g : ('type/finite_map/fmap' A B), x : A, y : B]: (f = (('const/finite_map/FUPDATE' A B) g (('const/pair/,' A B) x y))))))).
tt('thm/finite_map/SUBMAP_DOMSUB_', ax, ![A : $t, B : $t]: (![k : A, f : ('type/finite_map/fmap' A B)]: (('const/finite_map/SUBMAP' A B) (('const/finite_map/fdomsub' A B) f k) f))).
tt('thm/finite_map/FMERGE_DOMSUB_', ax, ![B : $t, A : $t]: (![m : (A > (A > A)), m1 : ('type/finite_map/fmap' B A), m2 : ('type/finite_map/fmap' B A), k : B]: ((('const/finite_map/fdomsub' B A) (('const/finite_map/FMERGE' A B) m m1 m2) k) = (('const/finite_map/FMERGE' A B) m (('const/finite_map/fdomsub' B A) m1 k) (('const/finite_map/fdomsub' B A) m2 k))))).
tt('thm/finite_map/SUBMAP_FUPDATE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/SUBMAP' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) g) = ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) g)) & (((('const/finite_map/FAPPLY' A B) g x) = y) & (('const/finite_map/SUBMAP' A B) (('const/finite_map/fdomsub' A B) f x) (('const/finite_map/fdomsub' A B) g x))))))).
tt('thm/finite_map/FUPDATE_LIST_', def, ![A : $t, B : $t]: (('const/finite_map/FUPDATE_LIST' A B) = (('const/list/FOLDL' ('type/pair/prod' A B) ('type/finite_map/fmap' A B)) ('const/finite_map/FUPDATE' A B)))).
tt('thm/finite_map/FUPDATE_LIST_THM_0', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUPDATE_LIST' A B) f ('const/list/NIL' ('type/pair/prod' A B))) = f))).
tt('thm/finite_map/FUPDATE_LIST_THM_e1', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), h : ('type/pair/prod' A B), t : ('type/list/list' ('type/pair/prod' A B))]: ((('const/finite_map/FUPDATE_LIST' A B) f (('const/list/CONS' ('type/pair/prod' A B)) h t)) = (('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE' A B) f h) t)))).
tt('thm/finite_map/FUPDATE_LIST_APPLY_NOT_MEM_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), f : ('type/finite_map/fmap' A B), k : A]: ((~ (('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) f kvl) k) = (('const/finite_map/FAPPLY' A B) f k))))).
tt('thm/finite_map/FUPDATE_LIST_APPEND_', ax, ![A : $t, B : $t]: (![kvl2 : ('type/list/list' ('type/pair/prod' A B)), kvl1 : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUPDATE_LIST' A B) fm (('const/list/APPEND' ('type/pair/prod' A B)) kvl1 kvl2)) = (('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE_LIST' A B) fm kvl1) kvl2)))).
tt('thm/finite_map/FUPDATE_FUPDATE_LIST_COMMUTES_', ax, ![B : $t, A : $t]: (![v : B, kvl : ('type/list/list' ('type/pair/prod' A B)), k : A, fm : ('type/finite_map/fmap' A B)]: ((~ (('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))) => ((('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) kvl) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/FUPDATE_LIST' A B) fm kvl) (('const/pair/,' A B) k v)))))).
tt('thm/finite_map/FUPDATE_FUPDATE_LIST_MEM_', ax, ![A : $t, B : $t]: (![v : B, kvl : ('type/list/list' ('type/pair/prod' A B)), k : A, fm : ('type/finite_map/fmap' A B)]: ((('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl))) => ((('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) kvl) = (('const/finite_map/FUPDATE_LIST' A B) fm kvl))))).
tt('thm/finite_map/FEVERY_FUPDATE_LIST_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A B) > $o)]: ((('const/list/ALL_DISTINCT' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)) => ((('const/finite_map/FEVERY' A B) P (('const/finite_map/FUPDATE_LIST' A B) fm kvl)) = ((('const/list/EVERY' ('type/pair/prod' A B)) P kvl) & (('const/finite_map/FEVERY' A B) P (('const/finite_map/DRESTRICT' A B) fm (('const/pred_set/COMPL' A) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))))))))).
tt('thm/finite_map/FUPDATE_LIST_APPLY_MEM_', ax, ![B : $t, A : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), f : ('type/finite_map/fmap' A B), k : A, v : B, n : 'type/num/num']: ((('const/prim_rec/<' n (('const/list/LENGTH' ('type/pair/prod' A B)) kvl)) & ((k = (('const/list/EL' A) n (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl))) & ((v = (('const/list/EL' B) n (('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) kvl))) & (![m : 'type/num/num']: ((('const/prim_rec/<' n m) & ('const/prim_rec/<' m (('const/list/LENGTH' ('type/pair/prod' A B)) kvl))) => (~ ((('const/list/EL' A) m (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)) = k))))))) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) f kvl) k) = v)))).
tt('thm/finite_map/FOLDL_FUPDATE_LIST_', ax, ![A : $t, C : $t, B : $t]: (![f1 : (A > B), f2 : (A > C), ls : ('type/list/list' A), a : ('type/finite_map/fmap' B C)]: ((('const/list/FOLDL' A ('type/finite_map/fmap' B C)) (^[fm : ('type/finite_map/fmap' B C), k : A]: (('const/finite_map/FUPDATE' B C) fm (('const/pair/,' B C) (f1 k) (f2 k)))) a ls) = (('const/finite_map/FUPDATE_LIST' B C) a (('const/list/MAP' A ('type/pair/prod' B C)) (^[k : A]: (('const/pair/,' B C) (f1 k) (f2 k))) ls))))).
tt('thm/finite_map/FUPDATE_LIST_SNOC_', ax, ![A : $t, B : $t]: (![xs : ('type/list/list' ('type/pair/prod' A B)), x : ('type/pair/prod' A B), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUPDATE_LIST' A B) fm (('const/list/SNOC' ('type/pair/prod' A B)) x xs)) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/FUPDATE_LIST' A B) fm xs) x)))).
tt('thm/finite_map/FUPD11_SAME_KEY_AND_BASE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), k : A, v1 : B, v2 : B]: (((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k v1)) = (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k v2))) = (v1 = v2)))).
tt('thm/finite_map/FUPD11_SAME_NEW_KEY_', ax, ![B : $t, A : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), k : A, v1 : B, v2 : B]: (((~ (('const/bool/IN' A) k (('const/finite_map/FDOM' A B) f1))) & (~ (('const/bool/IN' A) k (('const/finite_map/FDOM' A B) f2)))) => (((('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v1)) = (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v2))) = ((f1 = f2) & (v1 = v2)))))).
tt('thm/finite_map/SAME_KEY_UPDATES_DIFFER_', ax, ![B : $t, A : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), k : A, v1 : B, v2 : B]: ((~ (v1 = v2)) => (~ ((('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v1)) = (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v2))))))).
tt('thm/finite_map/FUPD11_SAME_BASE_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), k1 : A, v1 : B, k2 : A, v2 : B]: (((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k1 v1)) = (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k2 v2))) = (((k1 = k2) & (v1 = v2)) | ((~ (k1 = k2)) & ((('const/bool/IN' A) k1 (('const/finite_map/FDOM' A B) f)) & ((('const/bool/IN' A) k2 (('const/finite_map/FDOM' A B) f)) & (((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k1 v1)) = f) & ((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k2 v2)) = f))))))))).
tt('thm/finite_map/FUPD_SAME_KEY_UNWIND_', ax, ![B : $t, A : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), k : A, v1 : B, v2 : B]: (((('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v1)) = (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v2))) => ((v1 = v2) & (![v : B]: ((('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v)) = (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v)))))))).
tt('thm/finite_map/FUPD11_SAME_UPDATE_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), k : A, v : B]: (((('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v)) = (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v))) = ((('const/finite_map/DRESTRICT' A B) f1 (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) k ('const/pred_set/EMPTY' A)))) = (('const/finite_map/DRESTRICT' A B) f2 (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) k ('const/pred_set/EMPTY' A)))))))).
tt('thm/finite_map/FDOM_FUPDATE_LIST_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUPDATE_LIST' A B) fm kvl)) = (('const/pred_set/UNION' A) (('const/finite_map/FDOM' A B) fm) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))))).
tt('thm/finite_map/FUPDATE_LIST_SAME_UPDATE_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FUPDATE_LIST' A B) f1 kvl) = (('const/finite_map/FUPDATE_LIST' A B) f2 kvl)) = ((('const/finite_map/DRESTRICT' A B) f1 (('const/pred_set/COMPL' A) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))) = (('const/finite_map/DRESTRICT' A B) f2 (('const/pred_set/COMPL' A) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))))))).
tt('thm/finite_map/FUPDATE_LIST_SAME_KEYS_UNWIND_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), kvl1 : ('type/list/list' ('type/pair/prod' A B)), kvl2 : ('type/list/list' ('type/pair/prod' A B))]: ((((('const/finite_map/FUPDATE_LIST' A B) f1 kvl1) = (('const/finite_map/FUPDATE_LIST' A B) f2 kvl2)) & (((('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl1) = (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl2)) & (('const/list/ALL_DISTINCT' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl1)))) => ((kvl1 = kvl2) & (![kvl : ('type/list/list' ('type/pair/prod' A B))]: (((('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl) = (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl1)) => ((('const/finite_map/FUPDATE_LIST' A B) f1 kvl) = (('const/finite_map/FUPDATE_LIST' A B) f2 kvl)))))))).
tt('thm/finite_map/FMEQ_ENUMERATE_CASES_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), kvl : ('type/list/list' ('type/pair/prod' A B)), p : ('type/pair/prod' A B)]: (((('const/finite_map/FUPDATE' A B) f1 p) = (('const/finite_map/FUPDATE_LIST' A B) ('const/finite_map/FEMPTY' A B) kvl)) => (('const/bool/IN' ('type/pair/prod' A B)) p (('const/list/LIST_TO_SET' ('type/pair/prod' A B)) kvl))))).
tt('thm/finite_map/FMEQ_SINGLE_SIMPLE_ELIM_', ax, ![B : $t, A : $t]: (![P : (('type/finite_map/fmap' A B) > $o), k : A, v : B, ck : A, cv : B, nv : B]: ((?[fm : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) = (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) ck cv))) & (P (('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k nv))))) = ((k = ck) & ((v = cv) & (P (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) ck nv)))))))).
tt('thm/finite_map/FMEQ_SINGLE_SIMPLE_DISJ_ELIM_', ax, ![B : $t, A : $t]: (![fm : ('type/finite_map/fmap' A B), k : A, v : B, ck : A, cv : B]: (((('const/finite_map/FUPDATE' A B) fm (('const/pair/,' A B) k v)) = (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) ck cv))) = ((k = ck) & ((v = cv) & ((fm = ('const/finite_map/FEMPTY' A B)) | (?['v\'' : B]: (fm = (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) (('const/pair/,' A B) k 'v\'')))))))))).
tt('thm/finite_map/FUPDATE_PURGE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/fdomsub' A B) f x) (('const/pair/,' A B) x y))))).
tt('thm/finite_map/FMAP_MAP2_def_', def, ![A : $t, C : $t, B : $t]: (![f : (('type/pair/prod' A C) > B), m : ('type/finite_map/fmap' A C)]: ((('const/finite_map/FMAP_MAP2' A B C) f m) = (('const/finite_map/FUN_FMAP' A B) (^[x : A]: (f (('const/pair/,' A C) x (('const/finite_map/FAPPLY' A C) m x)))) (('const/finite_map/FDOM' A C) m))))).
tt('thm/finite_map/FMAP_MAP2_THM_0', ax, ![A : $t, C : $t, B : $t]: (![m : ('type/finite_map/fmap' A C), f : (('type/pair/prod' A C) > B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FMAP_MAP2' A B C) f m)) = (('const/finite_map/FDOM' A C) m)))).
tt('thm/finite_map/FMAP_MAP2_THM_e1', ax, ![A : $t, C : $t, B : $t]: (![m : ('type/finite_map/fmap' A C), f : (('type/pair/prod' A C) > B), x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) m)) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FMAP_MAP2' A B C) f m) x) = (f (('const/pair/,' A C) x (('const/finite_map/FAPPLY' A C) m x))))))).
tt('thm/finite_map/FMAP_MAP2_FEMPTY_', ax, ![A : $t, B : $t, C : $t]: (![f : (('type/pair/prod' A C) > B)]: ((('const/finite_map/FMAP_MAP2' A B C) f ('const/finite_map/FEMPTY' A C)) = ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FMAP_MAP2_FUPDATE_', ax, ![C : $t, A : $t, B : $t]: (![x : A, v : C, m : ('type/finite_map/fmap' A C), f : (('type/pair/prod' A C) > B)]: ((('const/finite_map/FMAP_MAP2' A B C) f (('const/finite_map/FUPDATE' A C) m (('const/pair/,' A C) x v))) = (('const/finite_map/FUPDATE' A B) (('const/finite_map/FMAP_MAP2' A B C) f m) (('const/pair/,' A B) x (f (('const/pair/,' A C) x v))))))).
tt('thm/finite_map/FEVERY_STRENGTHEN_THM_0', ax, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > $o)]: (('const/finite_map/FEVERY' A B) P ('const/finite_map/FEMPTY' A B)))).
tt('thm/finite_map/FEVERY_STRENGTHEN_THM_e1', ax, ![B : $t, A : $t]: (![y : B, x : A, f : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A B) > $o)]: (((('const/finite_map/FEVERY' A B) P f) & (P (('const/pair/,' A B) x y))) => (('const/finite_map/FEVERY' A B) P (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)))))).
tt('thm/finite_map/FUPDATE_ELIM_', ax, ![A : $t, B : $t]: (![k : A, v : B, f : ('type/finite_map/fmap' A B)]: (((('const/bool/IN' A) k (('const/finite_map/FDOM' A B) f)) & ((('const/finite_map/FAPPLY' A B) f k) = v)) => ((('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k v)) = f)))).
tt('thm/finite_map/FEVERY_DRESTRICT_COMPL_', ax, ![A : $t, B : $t]: (![v : B, s : (A > $o), k : A, f : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A B) > $o)]: ((('const/finite_map/FEVERY' A B) P (('const/finite_map/DRESTRICT' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) k v)) (('const/pred_set/COMPL' A) s))) = (((~ (('const/bool/IN' A) k s)) => (P (('const/pair/,' A B) k v))) & (('const/finite_map/FEVERY' A B) P (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) (('const/pred_set/INSERT' A) k s)))))))).
tt('thm/finite_map/FUNION_EQ_FEMPTY_', ax, ![A : $t, B : $t]: (![h1 : ('type/finite_map/fmap' A B), h2 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FUNION' A B) h1 h2) = ('const/finite_map/FEMPTY' A B)) = ((h1 = ('const/finite_map/FEMPTY' A B)) & (h2 = ('const/finite_map/FEMPTY' A B)))))).
tt('thm/finite_map/SUBMAP_FUNION_EQ_0', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), f3 : ('type/finite_map/fmap' A B)]: ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f2)) => ((('const/finite_map/SUBMAP' A B) f1 (('const/finite_map/FUNION' A B) f2 f3)) = (('const/finite_map/SUBMAP' A B) f1 f3))))).
tt('thm/finite_map/SUBMAP_FUNION_EQ_e1', ax, ![C : $t, D : $t]: (![f1 : ('type/finite_map/fmap' C D), f2 : ('type/finite_map/fmap' C D), f3 : ('type/finite_map/fmap' C D)]: ((('const/pred_set/DISJOINT' C) (('const/finite_map/FDOM' C D) f1) (('const/pred_set/DIFF' C) (('const/finite_map/FDOM' C D) f3) (('const/finite_map/FDOM' C D) f2))) => ((('const/finite_map/SUBMAP' C D) f1 (('const/finite_map/FUNION' C D) f2 f3)) = (('const/finite_map/SUBMAP' C D) f1 f2))))).
tt('thm/finite_map/SUBMAP_FUNION_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), f3 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/SUBMAP' A B) f1 f2) | ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f2)) & (('const/finite_map/SUBMAP' A B) f1 f3))) => (('const/finite_map/SUBMAP' A B) f1 (('const/finite_map/FUNION' A B) f2 f3))))).
tt('thm/finite_map/SUBMAP_FUNION_ID_0', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B)]: (('const/finite_map/SUBMAP' A B) f1 (('const/finite_map/FUNION' A B) f1 f2)))).
tt('thm/finite_map/SUBMAP_FUNION_ID_e1', ax, ![C : $t, D : $t]: (![f1 : ('type/finite_map/fmap' C D), f2 : ('type/finite_map/fmap' C D)]: ((('const/pred_set/DISJOINT' C) (('const/finite_map/FDOM' C D) f1) (('const/finite_map/FDOM' C D) f2)) => (('const/finite_map/SUBMAP' C D) f2 (('const/finite_map/FUNION' C D) f1 f2))))).
tt('thm/finite_map/FEMPTY_SUBMAP_', ax, ![A : $t, B : $t]: (![h : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) h ('const/finite_map/FEMPTY' A B)) = (h = ('const/finite_map/FEMPTY' A B))))).
tt('thm/finite_map/FUNION_EQ_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), f3 : ('type/finite_map/fmap' A B)]: (((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f2)) & (('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f3))) => (((('const/finite_map/FUNION' A B) f1 f2) = (('const/finite_map/FUNION' A B) f1 f3)) = (f2 = f3))))).
tt('thm/finite_map/FUNION_EQ_IMPL_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), f3 : ('type/finite_map/fmap' A B)]: (((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f2)) & ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f1) (('const/finite_map/FDOM' A B) f3)) & (f2 = f3))) => ((('const/finite_map/FUNION' A B) f1 f2) = (('const/finite_map/FUNION' A B) f1 f3))))).
tt('thm/finite_map/DOMSUB_FUNION_', ax, ![A : $t, B : $t]: (![k : A, g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/FUNION' A B) f g) k) = (('const/finite_map/FUNION' A B) (('const/finite_map/fdomsub' A B) f k) (('const/finite_map/fdomsub' A B) g k))))).
tt('thm/finite_map/FUNION_COMM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) f) (('const/finite_map/FDOM' A B) g)) => ((('const/finite_map/FUNION' A B) f g) = (('const/finite_map/FUNION' A B) g f))))).
tt('thm/finite_map/FUNION_ASSOC_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), h : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) f (('const/finite_map/FUNION' A B) g h)) = (('const/finite_map/FUNION' A B) (('const/finite_map/FUNION' A B) f g) h)))).
tt('thm/finite_map/DRESTRICT_FUNION_', ax, ![A : $t, B : $t]: (![h : ('type/finite_map/fmap' A B), s1 : (A > $o), s2 : (A > $o)]: ((('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) h s1) (('const/finite_map/DRESTRICT' A B) h s2)) = (('const/finite_map/DRESTRICT' A B) h (('const/pred_set/UNION' A) s1 s2))))).
tt('thm/finite_map/DRESTRICT_EQ_FUNION_', ax, ![A : $t, B : $t]: (![h : ('type/finite_map/fmap' A B), h1 : ('type/finite_map/fmap' A B), h2 : ('type/finite_map/fmap' A B)]: (((('const/pred_set/DISJOINT' A) (('const/finite_map/FDOM' A B) h1) (('const/finite_map/FDOM' A B) h2)) & ((('const/finite_map/FUNION' A B) h1 h2) = h)) => (h2 = (('const/finite_map/DRESTRICT' A B) h (('const/pred_set/COMPL' A) (('const/finite_map/FDOM' A B) h1))))))).
tt('thm/finite_map/IN_FDOM_FOLDR_UNION_', ax, ![A : $t, B : $t]: (![x : A, hL : ('type/list/list' ('type/finite_map/fmap' A B))]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/list/FOLDR' ('type/finite_map/fmap' A B) ('type/finite_map/fmap' A B)) ('const/finite_map/FUNION' A B) ('const/finite_map/FEMPTY' A B) hL))) = (?[h : ('type/finite_map/fmap' A B)]: ((('const/bool/IN' ('type/finite_map/fmap' A B)) h (('const/list/LIST_TO_SET' ('type/finite_map/fmap' A B)) hL)) & (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) h))))))).
tt('thm/finite_map/DRESTRICT_FUNION_DRESTRICT_COMPL_', ax, ![A : $t, B : $t]: (![s : (A > $o), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) f s) (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/COMPL' A) s))) = f))).
tt('thm/finite_map/DRESTRICT_IDEMPOT_', ax, ![A : $t, B : $t]: (![s : ('type/finite_map/fmap' A B), vs : (A > $o)]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/DRESTRICT' A B) s vs) vs) = (('const/finite_map/DRESTRICT' A B) s vs)))).
tt('thm/finite_map/SUBMAP_FUNION_ABSORPTION_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B)]: ((('const/finite_map/SUBMAP' A B) f g) = ((('const/finite_map/FUNION' A B) f g) = g)))).
tt('thm/finite_map/MAP_KEYS_witness_', ax, ![A : $t, C : $t, B : $t]: (('const/bool/LET' ((A > B) > (('type/finite_map/fmap' A C) > ('type/finite_map/fmap' B C))) $o) (^[m : ((A > B) > (('type/finite_map/fmap' A C) > ('type/finite_map/fmap' B C)))]: (![f : (A > B), fm : ('type/finite_map/fmap' A C)]: (((('const/finite_map/FDOM' B C) (m f fm)) = (('const/pred_set/IMAGE' A B) f (('const/finite_map/FDOM' A C) fm))) & ((('const/pred_set/INJ' A B) f (('const/finite_map/FDOM' A C) fm) ('const/pred_set/UNIV' B)) => (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) fm)) => ((('const/finite_map/FAPPLY' B C) (m f fm) (f x)) = (('const/finite_map/FAPPLY' A C) fm x)))))))) (^[f : (A > B), fm : ('type/finite_map/fmap' A C)]: (('const/bool/COND' ('type/finite_map/fmap' B C)) (('const/pred_set/INJ' A B) f (('const/finite_map/FDOM' A C) fm) ('const/pred_set/UNIV' B)) (('const/finite_map/f_o_f' B A C) fm (('const/finite_map/FUN_FMAP' B A) (('const/pred_set/LINV' A B) f (('const/finite_map/FDOM' A C) fm)) (('const/pred_set/IMAGE' A B) f (('const/finite_map/FDOM' A C) fm)))) (('const/finite_map/FUN_FMAP' B C) ('const/bool/ARB' (B > C)) (('const/pred_set/IMAGE' A B) f (('const/finite_map/FDOM' A C) fm))))))).
tt('thm/finite_map/MAP_KEYS_def_0', def, ![A : $t, C : $t, B : $t]: (![fm : ('type/finite_map/fmap' A C), f : (A > B)]: ((('const/finite_map/FDOM' B C) (('const/finite_map/MAP_KEYS' A B C) f fm)) = (('const/pred_set/IMAGE' A B) f (('const/finite_map/FDOM' A C) fm))))).
tt('thm/finite_map/MAP_KEYS_def_e1', def, ![A : $t, C : $t, B : $t]: (![fm : ('type/finite_map/fmap' A C), f : (A > B)]: ((('const/pred_set/INJ' A B) f (('const/finite_map/FDOM' A C) fm) ('const/pred_set/UNIV' B)) => (![x : A]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A C) fm)) => ((('const/finite_map/FAPPLY' B C) (('const/finite_map/MAP_KEYS' A B C) f fm) (f x)) = (('const/finite_map/FAPPLY' A C) fm x))))))).
tt('thm/finite_map/MAP_KEYS_FEMPTY_', ax, ![B : $t, C : $t, A : $t]: (![f : (A > B)]: ((('const/finite_map/MAP_KEYS' A B C) f ('const/finite_map/FEMPTY' A C)) = ('const/finite_map/FEMPTY' B C)))).
tt('thm/finite_map/MAP_KEYS_FUPDATE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), fm : ('type/finite_map/fmap' A C), k : A, v : C]: ((('const/pred_set/INJ' A B) f (('const/pred_set/INSERT' A) k (('const/finite_map/FDOM' A C) fm)) ('const/pred_set/UNIV' B)) => ((('const/finite_map/MAP_KEYS' A B C) f (('const/finite_map/FUPDATE' A C) fm (('const/pair/,' A C) k v))) = (('const/finite_map/FUPDATE' B C) (('const/finite_map/MAP_KEYS' A B C) f fm) (('const/pair/,' B C) (f k) v)))))).
tt('thm/finite_map/MAP_KEYS_using_LINV_', ax, ![A : $t, C : $t, B : $t]: (![f : (A > B), fm : ('type/finite_map/fmap' A C)]: ((('const/pred_set/INJ' A B) f (('const/finite_map/FDOM' A C) fm) ('const/pred_set/UNIV' B)) => ((('const/finite_map/MAP_KEYS' A B C) f fm) = (('const/finite_map/f_o_f' B A C) fm (('const/finite_map/FUN_FMAP' B A) (('const/pred_set/LINV' A B) f (('const/finite_map/FDOM' A C) fm)) (('const/pred_set/IMAGE' A B) f (('const/finite_map/FDOM' A C) fm)))))))).
tt('thm/finite_map/fmap_rel_def_', def, ![C : $t, B : $t, A : $t]: (![R : (A > (B > $o)), f1 : ('type/finite_map/fmap' C A), f2 : ('type/finite_map/fmap' C B)]: ((('const/finite_map/fmap_rel' A B C) R f1 f2) = (((('const/finite_map/FDOM' C B) f2) = (('const/finite_map/FDOM' C A) f1)) & (![x : C]: ((('const/bool/IN' C) x (('const/finite_map/FDOM' C A) f1)) => (R (('const/finite_map/FAPPLY' C A) f1 x) (('const/finite_map/FAPPLY' C B) f2 x)))))))).
tt('thm/finite_map/fmap_rel_FUPDATE_same_', ax, ![B : $t, C : $t, A : $t]: (![v2 : B, v1 : A, k : C, f2 : ('type/finite_map/fmap' C B), f1 : ('type/finite_map/fmap' C A), R : (A > (B > $o))]: (((('const/finite_map/fmap_rel' A B C) R f1 f2) & (R v1 v2)) => (('const/finite_map/fmap_rel' A B C) R (('const/finite_map/FUPDATE' C A) f1 (('const/pair/,' C A) k v1)) (('const/finite_map/FUPDATE' C B) f2 (('const/pair/,' C B) k v2)))))).
tt('thm/finite_map/fmap_rel_FUPDATE_LIST_same_', ax, ![C : $t, B : $t, A : $t]: (![R : (A > (B > $o)), ls1 : ('type/list/list' ('type/pair/prod' C A)), ls2 : ('type/list/list' ('type/pair/prod' C B)), f1 : ('type/finite_map/fmap' C A), f2 : ('type/finite_map/fmap' C B)]: (((('const/finite_map/fmap_rel' A B C) R f1 f2) & (((('const/list/MAP' ('type/pair/prod' C A) C) ('const/pair/FST' C A) ls1) = (('const/list/MAP' ('type/pair/prod' C B) C) ('const/pair/FST' C B) ls2)) & (('const/list/LIST_REL' A B) R (('const/list/MAP' ('type/pair/prod' C A) A) ('const/pair/SND' C A) ls1) (('const/list/MAP' ('type/pair/prod' C B) B) ('const/pair/SND' C B) ls2)))) => (('const/finite_map/fmap_rel' A B C) R (('const/finite_map/FUPDATE_LIST' C A) f1 ls1) (('const/finite_map/FUPDATE_LIST' C B) f2 ls2))))).
tt('thm/finite_map/fmap_rel_FEMPTY_', ax, ![C : $t, B : $t, A : $t]: (![R : (A > (B > $o))]: (('const/finite_map/fmap_rel' A B C) R ('const/finite_map/FEMPTY' C A) ('const/finite_map/FEMPTY' C B)))).
tt('thm/finite_map/fmap_rel_FEMPTY2_0', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' B A), R : (A > (A > $o))]: ((('const/finite_map/fmap_rel' A A B) R ('const/finite_map/FEMPTY' B A) f) = (f = ('const/finite_map/FEMPTY' B A))))).
tt('thm/finite_map/fmap_rel_FEMPTY2_e1', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' B A), R : (A > (A > $o))]: ((('const/finite_map/fmap_rel' A A B) R f ('const/finite_map/FEMPTY' B A)) = (f = ('const/finite_map/FEMPTY' B A))))).
tt('thm/finite_map/fmap_rel_refl_', ax, ![B : $t, A : $t]: (![x : ('type/finite_map/fmap' B A), R : (A > (A > $o))]: ((![x0 : A]: (R x0 x0)) => (('const/finite_map/fmap_rel' A A B) R x x)))).
tt('thm/finite_map/fmap_rel_FUNION_rels_', ax, ![C : $t, B : $t, A : $t]: (![f4 : ('type/finite_map/fmap' C B), f3 : ('type/finite_map/fmap' C A), f2 : ('type/finite_map/fmap' C B), f1 : ('type/finite_map/fmap' C A), R : (A > (B > $o))]: (((('const/finite_map/fmap_rel' A B C) R f1 f2) & (('const/finite_map/fmap_rel' A B C) R f3 f4)) => (('const/finite_map/fmap_rel' A B C) R (('const/finite_map/FUNION' C A) f1 f3) (('const/finite_map/FUNION' C B) f2 f4))))).
tt('thm/finite_map/fmap_rel_FUPDATE_I_', ax, ![B : $t, C : $t, A : $t]: (![v2 : B, v1 : A, k : C, f2 : ('type/finite_map/fmap' C B), f1 : ('type/finite_map/fmap' C A), R : (A > (B > $o))]: (((('const/finite_map/fmap_rel' A B C) R (('const/finite_map/fdomsub' C A) f1 k) (('const/finite_map/fdomsub' C B) f2 k)) & (R v1 v2)) => (('const/finite_map/fmap_rel' A B C) R (('const/finite_map/FUPDATE' C A) f1 (('const/pair/,' C A) k v1)) (('const/finite_map/FUPDATE' C B) f2 (('const/pair/,' C B) k v2)))))).
tt('thm/finite_map/fmap_rel_mono_', ax, ![C : $t, B : $t, A : $t]: (![f2 : ('type/finite_map/fmap' C B), f1 : ('type/finite_map/fmap' C A), R2 : (A > (B > $o)), R1 : (A > (B > $o))]: ((![x : A, y : B]: ((R1 x y) => (R2 x y))) => ((('const/finite_map/fmap_rel' A B C) R1 f1 f2) => (('const/finite_map/fmap_rel' A B C) R2 f1 f2))))).
tt('thm/finite_map/fmap_EQ_UPTO_def_', def, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), vs : (A > $o)]: ((('const/finite_map/fmap_EQ_UPTO' A B) f1 f2 vs) = (((('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f1) (('const/pred_set/COMPL' A) vs)) = (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f2) (('const/pred_set/COMPL' A) vs))) & (![x : A]: ((('const/bool/IN' A) x (('const/pred_set/INTER' A) (('const/finite_map/FDOM' A B) f1) (('const/pred_set/COMPL' A) vs))) => ((('const/finite_map/FAPPLY' A B) f1 x) = (('const/finite_map/FAPPLY' A B) f2 x)))))))).
tt('thm/finite_map/fmap_EQ_UPTO___EMPTY_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fmap_EQ_UPTO' A B) f1 f2 ('const/pred_set/EMPTY' A)) = (f1 = f2)))).
tt('thm/finite_map/fmap_EQ_UPTO___EQ_', ax, ![A : $t, B : $t]: (![vs : (A > $o), f : ('type/finite_map/fmap' A B)]: (('const/finite_map/fmap_EQ_UPTO' A B) f f vs))).
tt('thm/finite_map/fmap_EQ_UPTO___FUPDATE_BOTH_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), ks : (A > $o), k : A, v : B]: ((('const/finite_map/fmap_EQ_UPTO' A B) f1 f2 ks) => (('const/finite_map/fmap_EQ_UPTO' A B) (('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v)) (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v)) (('const/pred_set/DELETE' A) ks k))))).
tt('thm/finite_map/fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), ks : (A > $o), k : A, v : B]: ((('const/finite_map/fmap_EQ_UPTO' A B) f1 f2 ks) => (('const/finite_map/fmap_EQ_UPTO' A B) (('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v)) (('const/finite_map/FUPDATE' A B) f2 (('const/pair/,' A B) k v)) ks)))).
tt('thm/finite_map/fmap_EQ_UPTO___FUPDATE_SING_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), ks : (A > $o), k : A, v : B]: ((('const/finite_map/fmap_EQ_UPTO' A B) f1 f2 ks) => (('const/finite_map/fmap_EQ_UPTO' A B) (('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) k v)) f2 (('const/pred_set/INSERT' A) k ks))))).
tt('thm/finite_map/fmap_size_def_', def, ![A : $t, B : $t]: (![kz : (A > 'type/num/num'), vz : (B > 'type/num/num'), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/fmap_size' A B) kz vz fm) = (('const/pred_set/SUM_IMAGE' A) (^[k : A]: ('const/arithmetic/+' (kz k) (vz (('const/finite_map/FAPPLY' A B) fm k)))) (('const/finite_map/FDOM' A B) fm))))).
tt('thm/finite_map/o_f_FUNION_', ax, ![A : $t, C : $t, B : $t]: (![f2 : ('type/finite_map/fmap' A C), f1 : ('type/finite_map/fmap' A C), f : (C > B)]: ((('const/finite_map/o_f' A C B) f (('const/finite_map/FUNION' A C) f1 f2)) = (('const/finite_map/FUNION' A B) (('const/finite_map/o_f' A C B) f f1) (('const/finite_map/o_f' A C B) f f2))))).
tt('thm/finite_map/FDOM_FOLDR_DOMSUB_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' A), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/list/FOLDR' A ('type/finite_map/fmap' A B)) (^[k : A, m : ('type/finite_map/fmap' A B)]: (('const/finite_map/fdomsub' A B) m k)) fm ls)) = (('const/pred_set/DIFF' A) (('const/finite_map/FDOM' A B) fm) (('const/list/LIST_TO_SET' A) ls))))).
tt('thm/finite_map/FEVERY_SUBMAP_', ax, ![A : $t, B : $t]: (![fm0 : ('type/finite_map/fmap' A B), fm : ('type/finite_map/fmap' A B), P : (('type/pair/prod' A B) > $o)]: (((('const/finite_map/FEVERY' A B) P fm) & (('const/finite_map/SUBMAP' A B) fm0 fm)) => (('const/finite_map/FEVERY' A B) P fm0)))).
tt('thm/finite_map/FEVERY_ALL_FLOOKUP_', ax, ![B : $t, A : $t]: (![P : (('type/pair/prod' A B) > $o), f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FEVERY' A B) P f) = (![k : A, v : B]: (((('const/finite_map/FLOOKUP' A B) f k) = (('const/option/SOME' B) v)) => (P (('const/pair/,' A B) k v))))))).
tt('thm/finite_map/FUPDATE_LIST_CANCEL_', ax, ![A : $t, B : $t]: (![ls1 : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B), ls2 : ('type/list/list' ('type/pair/prod' A B))]: ((![k : A]: ((('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) ls1))) => (('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) ls2))))) => ((('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE_LIST' A B) fm ls1) ls2) = (('const/finite_map/FUPDATE_LIST' A B) fm ls2))))).
tt('thm/finite_map/FUPDATE_EQ_FUNION_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), kv : ('type/pair/prod' A B)]: ((('const/finite_map/FUPDATE' A B) fm kv) = (('const/finite_map/FUNION' A B) (('const/finite_map/FUPDATE' A B) ('const/finite_map/FEMPTY' A B) kv) fm)))).
tt('thm/finite_map/FUPDATE_LIST_APPEND_COMMUTES_', ax, ![A : $t, B : $t]: (![l1 : ('type/list/list' ('type/pair/prod' A B)), l2 : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: ((('const/pred_set/DISJOINT' A) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l1)) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l2))) => ((('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE_LIST' A B) fm l1) l2) = (('const/finite_map/FUPDATE_LIST' A B) (('const/finite_map/FUPDATE_LIST' A B) fm l2) l1))))).
tt('thm/finite_map/fmap_rel_OPTREL_FLOOKUP_', ax, ![C : $t, B : $t, A : $t]: (![f2 : ('type/finite_map/fmap' C B), f1 : ('type/finite_map/fmap' C A), R : (A > (B > $o))]: ((('const/finite_map/fmap_rel' A B C) R f1 f2) = (![k : C]: (('const/option/OPTREL' A B) R (('const/finite_map/FLOOKUP' C A) f1 k) (('const/finite_map/FLOOKUP' C B) f2 k)))))).
tt('thm/finite_map/FLOOKUP_DRESTRICT_', ax, ![B : $t, A : $t]: (![fm : ('type/finite_map/fmap' A B), s : (A > $o), k : A]: ((('const/finite_map/FLOOKUP' A B) (('const/finite_map/DRESTRICT' A B) fm s) k) = (('const/bool/COND' ('type/option/option' B)) (('const/bool/IN' A) k s) (('const/finite_map/FLOOKUP' A B) fm k) ('const/option/NONE' B))))).
tt('thm/finite_map/IMAGE_FRANGE_', ax, ![C : $t, A : $t, B : $t]: (![f : (A > B), fm : ('type/finite_map/fmap' C A)]: ((('const/pred_set/IMAGE' A B) f (('const/finite_map/FRANGE' C A) fm)) = (('const/finite_map/FRANGE' C B) (('const/finite_map/o_f' C A B) f fm))))).
tt('thm/finite_map/SUBMAP_mono_FUPDATE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : A, y : B]: ((('const/finite_map/SUBMAP' A B) (('const/finite_map/fdomsub' A B) f x) (('const/finite_map/fdomsub' A B) g x)) => (('const/finite_map/SUBMAP' A B) (('const/finite_map/FUPDATE' A B) f (('const/pair/,' A B) x y)) (('const/finite_map/FUPDATE' A B) g (('const/pair/,' A B) x y)))))).
tt('thm/finite_map/SUBMAP_DOMSUB_gen_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), k : A]: ((('const/finite_map/SUBMAP' A B) (('const/finite_map/fdomsub' A B) f k) g) = (('const/finite_map/SUBMAP' A B) (('const/finite_map/fdomsub' A B) f k) (('const/finite_map/fdomsub' A B) g k))))).
tt('thm/finite_map/DOMSUB_SUBMAP_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), g : ('type/finite_map/fmap' A B), x : A]: (((('const/finite_map/SUBMAP' A B) f g) & (~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)))) => (('const/finite_map/SUBMAP' A B) f (('const/finite_map/fdomsub' A B) g x))))).
tt('thm/finite_map/DRESTRICT_DOMSUB_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B), s : (A > $o), k : A]: ((('const/finite_map/fdomsub' A B) (('const/finite_map/DRESTRICT' A B) f s) k) = (('const/finite_map/DRESTRICT' A B) f (('const/pred_set/DELETE' A) s k))))).
tt('thm/finite_map/DRESTRICT_SUBSET_SUBMAP_gen_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), s : (A > $o), t : (A > $o)]: (((('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f1 s) (('const/finite_map/DRESTRICT' A B) f2 s)) & (('const/pred_set/SUBSET' A) t s)) => (('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f1 t) (('const/finite_map/DRESTRICT' A B) f2 t))))).
tt('thm/finite_map/DRESTRICT_FUNION_SAME_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), s : (A > $o)]: ((('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) fm s) fm) = fm))).
tt('thm/finite_map/DRESTRICT_EQ_DRESTRICT_SAME_', ax, ![A : $t, B : $t]: (![s : (A > $o), f2 : ('type/finite_map/fmap' A B), f1 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/DRESTRICT' A B) f1 s) = (('const/finite_map/DRESTRICT' A B) f2 s)) = (((('const/pred_set/INTER' A) s (('const/finite_map/FDOM' A B) f1)) = (('const/pred_set/INTER' A) s (('const/finite_map/FDOM' A B) f2))) & (![x : A]: (((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f1)) & (('const/bool/IN' A) x s)) => ((('const/finite_map/FAPPLY' A B) f1 x) = (('const/finite_map/FAPPLY' A B) f2 x)))))))).
tt('thm/finite_map/FOLDL2_FUPDATE_LIST_', ax, ![B : $t, A : $t, D : $t, C : $t]: (![f1 : (A > (B > C)), f2 : (A > (B > D)), bs : ('type/list/list' A), cs : ('type/list/list' B), a : ('type/finite_map/fmap' C D)]: (((('const/list/LENGTH' A) bs) = (('const/list/LENGTH' B) cs)) => ((('const/list/FOLDL2' ('type/finite_map/fmap' C D) A B) (^[fm : ('type/finite_map/fmap' C D), b : A, c : B]: (('const/finite_map/FUPDATE' C D) fm (('const/pair/,' C D) (f1 b c) (f2 b c)))) a bs cs) = (('const/finite_map/FUPDATE_LIST' C D) a (('const/list/ZIP' C D) (('const/pair/,' ('type/list/list' C) ('type/list/list' D)) (('const/list/MAP2' C A B) f1 bs cs) (('const/list/MAP2' D A B) f2 bs cs)))))))).
tt('thm/finite_map/FOLDL2_FUPDATE_LIST_paired_', ax, ![B : $t, C : $t, A : $t, E : $t, D : $t]: (![f1 : (A > (B > (C > D))), f2 : (A > (B > (C > E))), bs : ('type/list/list' A), cs : ('type/list/list' ('type/pair/prod' B C)), a : ('type/finite_map/fmap' D E)]: (((('const/list/LENGTH' A) bs) = (('const/list/LENGTH' ('type/pair/prod' B C)) cs)) => ((('const/list/FOLDL2' ('type/finite_map/fmap' D E) A ('type/pair/prod' B C)) (^[fm : ('type/finite_map/fmap' D E), b : A]: (('const/pair/UNCURRY' B C ('type/finite_map/fmap' D E)) (^[c : B, d : C]: (('const/finite_map/FUPDATE' D E) fm (('const/pair/,' D E) (f1 b c d) (f2 b c d)))))) a bs cs) = (('const/finite_map/FUPDATE_LIST' D E) a (('const/list/ZIP' D E) (('const/pair/,' ('type/list/list' D) ('type/list/list' E)) (('const/list/MAP2' D A ('type/pair/prod' B C)) (^[b : A]: (('const/pair/UNCURRY' B C D) (f1 b))) bs cs) (('const/list/MAP2' E A ('type/pair/prod' B C)) (^[b : A]: (('const/pair/UNCURRY' B C E) (f2 b))) bs cs)))))))).
tt('thm/finite_map/DRESTRICT_FUNION_SUBSET_', ax, ![A : $t, B : $t]: (![s2 : (A > $o), s1 : (A > $o), g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B)]: ((('const/pred_set/SUBSET' A) s2 s1) => (?[h : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) f s1) g) = (('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) f s2) h)))))).
tt('thm/finite_map/FUPDATE_LIST_APPLY_NOT_MEM_matchable_', ax, ![B : $t, A : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), f : ('type/finite_map/fmap' A B), k : A, v : B]: (((~ (('const/bool/IN' A) k (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))) & (v = (('const/finite_map/FAPPLY' A B) f k))) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) f kvl) k) = v)))).
tt('thm/finite_map/FUPDATE_LIST_APPLY_HO_THM_', ax, ![B : $t, A : $t]: (![P : (A > $o), f : ('type/finite_map/fmap' B A), kvl : ('type/list/list' ('type/pair/prod' B A)), k : B]: (((?[n : 'type/num/num']: (('const/prim_rec/<' n (('const/list/LENGTH' ('type/pair/prod' B A)) kvl)) & ((k = (('const/list/EL' B) n (('const/list/MAP' ('type/pair/prod' B A) B) ('const/pair/FST' B A) kvl))) & ((P (('const/list/EL' A) n (('const/list/MAP' ('type/pair/prod' B A) A) ('const/pair/SND' B A) kvl))) & (![m : 'type/num/num']: ((('const/prim_rec/<' n m) & ('const/prim_rec/<' m (('const/list/LENGTH' ('type/pair/prod' B A)) kvl))) => (~ ((('const/list/EL' B) m (('const/list/MAP' ('type/pair/prod' B A) B) ('const/pair/FST' B A) kvl)) = k)))))))) | ((~ (('const/bool/IN' B) k (('const/list/LIST_TO_SET' B) (('const/list/MAP' ('type/pair/prod' B A) B) ('const/pair/FST' B A) kvl)))) & (P (('const/finite_map/FAPPLY' B A) f k)))) => (P (('const/finite_map/FAPPLY' B A) (('const/finite_map/FUPDATE_LIST' B A) f kvl) k))))).
tt('thm/finite_map/FUPDATE_SAME_APPLY_', ax, ![A : $t, B : $t]: (![x : A, kv : ('type/pair/prod' A B), fm2 : ('type/finite_map/fmap' A B), fm1 : ('type/finite_map/fmap' A B)]: (((x = (('const/pair/FST' A B) kv)) | ((('const/finite_map/FAPPLY' A B) fm1 x) = (('const/finite_map/FAPPLY' A B) fm2 x))) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE' A B) fm1 kv) x) = (('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE' A B) fm2 kv) x))))).
tt('thm/finite_map/FUPDATE_SAME_LIST_APPLY_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), fm1 : ('type/finite_map/fmap' A B), fm2 : ('type/finite_map/fmap' A B), x : A]: ((('const/bool/IN' A) x (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl))) => ((('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) fm1 kvl) x) = (('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) fm2 kvl) x))))).
tt('thm/finite_map/FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM_', ax, ![B : $t, A : $t]: (![P : (A > $o), ls : ('type/list/list' ('type/pair/prod' B A)), k : B, v : A, fm : ('type/finite_map/fmap' B A)]: (((('const/list/ALL_DISTINCT' B) (('const/list/MAP' ('type/pair/prod' B A) B) ('const/pair/FST' B A) ls)) & ((('const/bool/IN' ('type/pair/prod' B A)) (('const/pair/,' B A) k v) (('const/list/LIST_TO_SET' ('type/pair/prod' B A)) ls)) & (P v))) => (P (('const/finite_map/FAPPLY' B A) (('const/finite_map/FUPDATE_LIST' B A) fm ls) k))))).
tt('thm/finite_map/FUPDATE_LIST_ALL_DISTINCT_REVERSE_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/ALL_DISTINCT' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) ls)) => (![fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FUPDATE_LIST' A B) fm (('const/list/REVERSE' ('type/pair/prod' A B)) ls)) = (('const/finite_map/FUPDATE_LIST' A B) fm ls)))))).
tt('thm/finite_map/IN_FRANGE_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), v : B]: ((('const/bool/IN' B) v (('const/finite_map/FRANGE' A B) f)) = (?[k : A]: ((('const/bool/IN' A) k (('const/finite_map/FDOM' A B) f)) & ((('const/finite_map/FAPPLY' A B) f k) = v)))))).
tt('thm/finite_map/IN_FRANGE_FLOOKUP_', ax, ![B : $t, A : $t]: (![f : ('type/finite_map/fmap' A B), v : B]: ((('const/bool/IN' B) v (('const/finite_map/FRANGE' A B) f)) = (?[k : A]: ((('const/finite_map/FLOOKUP' A B) f k) = (('const/option/SOME' B) v)))))).
tt('thm/finite_map/FRANGE_FUPDATE_LIST_SUBSET_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: (('const/pred_set/SUBSET' B) (('const/finite_map/FRANGE' A B) (('const/finite_map/FUPDATE_LIST' A B) fm ls)) (('const/pred_set/UNION' B) (('const/finite_map/FRANGE' A B) fm) (('const/list/LIST_TO_SET' B) (('const/list/MAP' ('type/pair/prod' A B) B) ('const/pair/SND' A B) ls)))))).
tt('thm/finite_map/IN_FRANGE_FUPDATE_LIST_suff_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' ('type/pair/prod' B A)), fm : ('type/finite_map/fmap' B A), P : (A > $o)]: (((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) fm)) => (P v))) & (![v : A]: ((('const/bool/IN' A) v (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' B A) A) ('const/pair/SND' B A) ls))) => (P v)))) => (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) (('const/finite_map/FUPDATE_LIST' B A) fm ls))) => (P v)))))).
tt('thm/finite_map/FRANGE_FUNION_SUBSET_', ax, ![B : $t, A : $t]: (![f2 : ('type/finite_map/fmap' B A), f1 : ('type/finite_map/fmap' B A)]: (('const/pred_set/SUBSET' A) (('const/finite_map/FRANGE' B A) (('const/finite_map/FUNION' B A) f1 f2)) (('const/pred_set/UNION' A) (('const/finite_map/FRANGE' B A) f1) (('const/finite_map/FRANGE' B A) f2))))).
tt('thm/finite_map/IN_FRANGE_FUNION_suff_', ax, ![A : $t, B : $t]: (![f2 : ('type/finite_map/fmap' B A), f1 : ('type/finite_map/fmap' B A), P : (A > $o)]: (((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) f1)) => (P v))) & (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) f2)) => (P v)))) => (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) (('const/finite_map/FUNION' B A) f1 f2))) => (P v)))))).
tt('thm/finite_map/FRANGE_DOMSUB_SUBSET_', ax, ![B : $t, A : $t]: (![k : B, fm : ('type/finite_map/fmap' B A)]: (('const/pred_set/SUBSET' A) (('const/finite_map/FRANGE' B A) (('const/finite_map/fdomsub' B A) fm k)) (('const/finite_map/FRANGE' B A) fm)))).
tt('thm/finite_map/IN_FRANGE_DOMSUB_suff_', ax, ![A : $t, B : $t]: (![k : B, fm : ('type/finite_map/fmap' B A), P : (A > $o)]: ((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) fm)) => (P v))) => (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) (('const/finite_map/fdomsub' B A) fm k))) => (P v)))))).
tt('thm/finite_map/IN_FRANGE_DRESTRICT_suff_', ax, ![A : $t, B : $t]: (![s : (B > $o), fm : ('type/finite_map/fmap' B A), P : (A > $o)]: ((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) fm)) => (P v))) => (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) (('const/finite_map/DRESTRICT' B A) fm s))) => (P v)))))).
tt('thm/finite_map/FRANGE_FUPDATE_SUBSET_', ax, ![A : $t, B : $t]: (![kv : ('type/pair/prod' B A), fm : ('type/finite_map/fmap' B A)]: (('const/pred_set/SUBSET' A) (('const/finite_map/FRANGE' B A) (('const/finite_map/FUPDATE' B A) fm kv)) (('const/pred_set/UNION' A) (('const/finite_map/FRANGE' B A) fm) (('const/pred_set/INSERT' A) (('const/pair/SND' B A) kv) ('const/pred_set/EMPTY' A)))))).
tt('thm/finite_map/IN_FRANGE_FUPDATE_suff_', ax, ![A : $t, B : $t]: (![kv : ('type/pair/prod' B A), fm : ('type/finite_map/fmap' B A), P : (A > $o)]: (((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) fm)) => (P v))) & (P (('const/pair/SND' B A) kv))) => (![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) (('const/finite_map/FUPDATE' B A) fm kv))) => (P v)))))).
tt('thm/finite_map/IN_FRANGE_o_f_suff_', ax, ![C : $t, B : $t, A : $t]: (![fm : ('type/finite_map/fmap' B A), f : (A > C), P : (C > $o)]: ((![v : A]: ((('const/bool/IN' A) v (('const/finite_map/FRANGE' B A) fm)) => (P (f v)))) => (![v : C]: ((('const/bool/IN' C) v (('const/finite_map/FRANGE' B C) (('const/finite_map/o_f' B A C) f fm))) => (P v)))))).
tt('thm/finite_map/DRESTRICT_SUBMAP_gen_', ax, ![A : $t, B : $t]: (![g : ('type/finite_map/fmap' A B), f : ('type/finite_map/fmap' A B), P : (A > $o)]: ((('const/finite_map/SUBMAP' A B) f g) => (('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f P) g)))).
tt('thm/finite_map/DRESTRICT_SUBSET_SUBMAP_', ax, ![A : $t, B : $t]: (![s2 : (A > $o), s1 : (A > $o), f : ('type/finite_map/fmap' A B)]: ((('const/pred_set/SUBSET' A) s1 s2) => (('const/finite_map/SUBMAP' A B) (('const/finite_map/DRESTRICT' A B) f s1) (('const/finite_map/DRESTRICT' A B) f s2))))).
tt('thm/finite_map/DRESTRICTED_FUNION_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), s : (A > $o)]: ((('const/finite_map/DRESTRICT' A B) (('const/finite_map/FUNION' A B) f1 f2) s) = (('const/finite_map/FUNION' A B) (('const/finite_map/DRESTRICT' A B) f1 s) (('const/finite_map/DRESTRICT' A B) f2 (('const/pred_set/DIFF' A) s (('const/finite_map/FDOM' A B) f1))))))).
tt('thm/finite_map/FRANGE_DRESTRICT_SUBSET_', ax, ![B : $t, A : $t]: (![s : (B > $o), fm : ('type/finite_map/fmap' B A)]: (('const/pred_set/SUBSET' A) (('const/finite_map/FRANGE' B A) (('const/finite_map/DRESTRICT' B A) fm s)) (('const/finite_map/FRANGE' B A) fm)))).
tt('thm/finite_map/DRESTRICT_FDOM_', ax, ![A : $t, B : $t]: (![f : ('type/finite_map/fmap' A B)]: ((('const/finite_map/DRESTRICT' A B) f (('const/finite_map/FDOM' A B) f)) = f))).
tt('thm/finite_map/DRESTRICT_SUBSET_', ax, ![A : $t, B : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' A B), s : (A > $o), t : (A > $o)]: ((((('const/finite_map/DRESTRICT' A B) f1 s) = (('const/finite_map/DRESTRICT' A B) f2 s)) & (('const/pred_set/SUBSET' A) t s)) => ((('const/finite_map/DRESTRICT' A B) f1 t) = (('const/finite_map/DRESTRICT' A B) f2 t))))).
tt('thm/finite_map/f_o_f_FUPDATE_compose_', ax, ![B : $t, C : $t, A : $t]: (![f1 : ('type/finite_map/fmap' A B), f2 : ('type/finite_map/fmap' C A), k : C, x : A, v : B]: (((~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f1))) & (~ (('const/bool/IN' A) x (('const/finite_map/FRANGE' C A) f2)))) => ((('const/finite_map/f_o_f' C A B) (('const/finite_map/FUPDATE' A B) f1 (('const/pair/,' A B) x v)) (('const/finite_map/FUPDATE' C A) f2 (('const/pair/,' C A) k x))) = (('const/finite_map/FUPDATE' C B) (('const/finite_map/f_o_f' C A B) f1 f2) (('const/pair/,' C B) k v)))))).
tt('thm/finite_map/fmap_rel_trans_', ax, ![B : $t, A : $t]: (![R : (A > (A > $o))]: ((![x : A, y : A, z : A]: (((R x y) & (R y z)) => (R x z))) => (![x : ('type/finite_map/fmap' B A), y : ('type/finite_map/fmap' B A), z : ('type/finite_map/fmap' B A)]: (((('const/finite_map/fmap_rel' A A B) R x y) & (('const/finite_map/fmap_rel' A A B) R y z)) => (('const/finite_map/fmap_rel' A A B) R x z)))))).
tt('thm/finite_map/fmap_rel_sym_', ax, ![B : $t, A : $t]: (![R : (A > (A > $o))]: ((![x : A, y : A]: ((R x y) => (R y x))) => (![x : ('type/finite_map/fmap' B A), y : ('type/finite_map/fmap' B A)]: ((('const/finite_map/fmap_rel' A A B) R x y) => (('const/finite_map/fmap_rel' A A B) R y x)))))).
tt('thm/finite_map/fmap_eq_flookup_', ax, ![A : $t, B : $t]: (![m1 : ('type/finite_map/fmap' A B), m2 : ('type/finite_map/fmap' A B)]: ((m1 = m2) = (![k : A]: ((('const/finite_map/FLOOKUP' A B) m1 k) = (('const/finite_map/FLOOKUP' A B) m2 k)))))).
tt('thm/finite_map/fupdate_list_map_', ax, ![A : $t, B : $t, C : $t, D : $t]: (![l : ('type/list/list' ('type/pair/prod' A B)), f : (B > C), x : A, y : D]: ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) (('const/finite_map/FUPDATE_LIST' A B) ('const/finite_map/FEMPTY' A B) l))) => ((('const/finite_map/FAPPLY' A C) (('const/finite_map/FUPDATE_LIST' A C) ('const/finite_map/FEMPTY' A C) (('const/list/MAP' ('type/pair/prod' A B) ('type/pair/prod' A C)) (('const/pair/UNCURRY' A B ('type/pair/prod' A C)) (^[a : A, b : B]: (('const/pair/,' A C) a (f b)))) l)) x) = (f (('const/finite_map/FAPPLY' A B) (('const/finite_map/FUPDATE_LIST' A B) ('const/finite_map/FEMPTY' A B) l) x)))))).
tt('thm/finite_map/fdom_fupdate_list2_', ax, ![A : $t, B : $t]: (![kvl : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: ((('const/finite_map/FDOM' A B) (('const/finite_map/FUPDATE_LIST' A B) fm kvl)) = (('const/pred_set/UNION' A) (('const/pred_set/DIFF' A) (('const/finite_map/FDOM' A B) fm) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl))) (('const/list/LIST_TO_SET' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) kvl)))))).
tt('thm/finite_map/flookup_thm_0', ax, ![A : $t, B : $t]: (![x : A, f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FLOOKUP' A B) f x) = ('const/option/NONE' B)) = (~ (('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)))))).
tt('thm/finite_map/flookup_thm_e1', ax, ![B : $t, A : $t]: (![x : A, v : B, f : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FLOOKUP' A B) f x) = (('const/option/SOME' B) v)) = ((('const/bool/IN' A) x (('const/finite_map/FDOM' A B) f)) & ((('const/finite_map/FAPPLY' A B) f x) = v))))).
tt('thm/finite_map/FUPDATE_EQ_FUPDATE_LIST_', ax, ![A : $t, B : $t]: (![fm : ('type/finite_map/fmap' A B), kv : ('type/pair/prod' A B)]: ((('const/finite_map/FUPDATE' A B) fm kv) = (('const/finite_map/FUPDATE_LIST' A B) fm (('const/list/CONS' ('type/pair/prod' A B)) kv ('const/list/NIL' ('type/pair/prod' A B))))))).
tt('thm/finite_map/fmap_inverse_def_', def, ![A : $t, B : $t]: (![m1 : ('type/finite_map/fmap' A B), m2 : ('type/finite_map/fmap' B A)]: ((('const/finite_map/fmap_inverse' A B) m1 m2) = (![k : A]: ((('const/bool/IN' A) k (('const/finite_map/FDOM' A B) m1)) => (?[v : B]: (((('const/finite_map/FLOOKUP' A B) m1 k) = (('const/option/SOME' B) v)) & ((('const/finite_map/FLOOKUP' B A) m2 v) = (('const/option/SOME' A) k))))))))).
tt('thm/finite_map/fupdate_list_foldr_', ax, ![A : $t, B : $t]: (![m : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/FOLDR' ('type/pair/prod' A B) ('type/finite_map/fmap' A B)) (('const/pair/UNCURRY' A B (('type/finite_map/fmap' A B) > ('type/finite_map/fmap' A B))) (^[k : A, v : B, env : ('type/finite_map/fmap' A B)]: (('const/finite_map/FUPDATE' A B) env (('const/pair/,' A B) k v)))) m l) = (('const/finite_map/FUPDATE_LIST' A B) m (('const/list/REVERSE' ('type/pair/prod' A B)) l))))).
tt('thm/finite_map/fupdate_list_foldl_', ax, ![A : $t, B : $t]: (![m : ('type/finite_map/fmap' A B), l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/FOLDL' ('type/pair/prod' A B) ('type/finite_map/fmap' A B)) (^[env : ('type/finite_map/fmap' A B)]: (('const/pair/UNCURRY' A B ('type/finite_map/fmap' A B)) (^[k : A, v : B]: (('const/finite_map/FUPDATE' A B) env (('const/pair/,' A B) k v))))) m l) = (('const/finite_map/FUPDATE_LIST' A B) m l)))).
tt('thm/finite_map/fmap_to_list_', ax, ![A : $t, B : $t]: (![m : ('type/finite_map/fmap' A B)]: (?[l : ('type/list/list' ('type/pair/prod' A B))]: ((('const/list/ALL_DISTINCT' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) l)) & (m = (('const/finite_map/FUPDATE_LIST' A B) ('const/finite_map/FEMPTY' A B) l)))))).
tt('thm/finite_map/disjoint_drestrict_', ax, ![A : $t, B : $t]: (![s : (A > $o), m : ('type/finite_map/fmap' A B)]: ((('const/pred_set/DISJOINT' A) s (('const/finite_map/FDOM' A B) m)) => ((('const/finite_map/DRESTRICT' A B) m (('const/pred_set/COMPL' A) s)) = m)))).
tt('thm/finite_map/drestrict_iter_list_', ax, ![A : $t, B : $t]: (![m : ('type/finite_map/fmap' A B), l : ('type/list/list' A)]: ((('const/list/FOLDR' A ('type/finite_map/fmap' A B)) (^[k : A, m0 : ('type/finite_map/fmap' A B)]: (('const/finite_map/fdomsub' A B) m0 k)) m l) = (('const/finite_map/DRESTRICT' A B) m (('const/pred_set/COMPL' A) (('const/list/LIST_TO_SET' A) l)))))).
tt('thm/finite_map/fevery_funion_', ax, ![A : $t, B : $t]: (![P : (('type/pair/prod' A B) > $o), m1 : ('type/finite_map/fmap' A B), m2 : ('type/finite_map/fmap' A B)]: (((('const/finite_map/FEVERY' A B) P m1) & (('const/finite_map/FEVERY' A B) P m2)) => (('const/finite_map/FEVERY' A B) P (('const/finite_map/FUNION' A B) m1 m2))))).
tt('thm/finite_map/FUPDATE_LIST_ALL_DISTINCT_PERM_', ax, ![A : $t, B : $t]: (![ls : ('type/list/list' ('type/pair/prod' A B)), 'ls\'' : ('type/list/list' ('type/pair/prod' A B)), fm : ('type/finite_map/fmap' A B)]: (((('const/list/ALL_DISTINCT' A) (('const/list/MAP' ('type/pair/prod' A B) A) ('const/pair/FST' A B) ls)) & (('const/sorting/PERM' ('type/pair/prod' A B)) ls 'ls\'')) => ((('const/finite_map/FUPDATE_LIST' A B) fm ls) = (('const/finite_map/FUPDATE_LIST' A B) fm 'ls\''))))).
