(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module F = Filename
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val out_int: int -> unit
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module A = Array
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val from_uri: string -> string -> NUri.uri -> unit
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module A = Array
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val objects: unit -> unit
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module L = List
let malformed () =
failwith "probe: malformed term"
+let add_name str =
+ let u = U.uri_of_string str in
+ if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str;
+ O.names := US.add u !O.names
+
let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
let add_ind n = O.add_xflavour n `Inductive
L.fold_left map cts ts
let set_funs c rfs cts =
- let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
+ let map cts (_, s, _, t0, t1) =
+ add_name s;
+ set_list c [t0; t1] cts
+ in
L.fold_left map cts rfs
-let set_type c cts (_, _, t, css) =
- let map cts (_, _, t) = (c, t) :: cts in
- (c, t) :: L.fold_left map cts css
+let set_type c cts (_, s, t, css) =
+ let map cts (_, s, t) = add_name s; (c, t) :: cts in
+ add_name s; (c, t) :: L.fold_left map cts css
let inc st = {st with c = succ st.c}
let st = {c; u} in
let _, _, _, _, obj = E.get_checked_obj status u in
let st = match obj with
- | C.Constant (_, _, None, t, m) ->
- add_attr 1 m;
+ | C.Constant (_, s, None, t, m) ->
+ add_name s; add_attr 1 m;
scan_term (inc st) [[], t]
- | C.Constant (_, _, Some t0, t1, m) ->
- add_attr 1 m;
+ | C.Constant (_, s, Some t0, t1, m) ->
+ add_name s; add_attr 1 m;
scan_term (inc st) (set_list [] [t0; t1] [])
| C.Fixpoint (_, rfs, m) ->
add_attr (L.length rfs) m;
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val scan: unit -> unit
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module A = Array
let default_srcs = US.empty
+let default_names = US.empty
+
let default_remove = []
let default_exclude = []
let srcs = ref default_srcs
+let names = ref default_names
+
let remove = ref default_remove
let exclude = ref default_exclude
let clear () =
R.clear (); A.iteri clear_slot slot;
- objs := default_objs; srcs := default_srcs; remove := default_remove;
- exclude := default_exclude; net := default_net;
+ objs := default_objs; srcs := default_srcs; names := default_names;
+ remove := default_remove; exclude := default_exclude; net := default_net;
chars := default_chars; debug_lexer := default_debug_lexer;
no_devel := default_no_devel; no_init := default_no_init;
deps := UPS.empty
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
type def_xflavour = [ NCic.def_flavour
| `Inductive
]
-val add_xflavour: int -> def_xflavour -> unit
+val add_xflavour: int -> def_xflavour -> unit
val iter_xflavours: (int -> unit) -> unit
val srcs: NUri.UriSet.t ref
+val names: NUri.UriSet.t ref
+
val remove: string list ref
val exclude: NCic.source list ref
(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
module A = Arg
let out_f () = O.iter_xflavours E.out_int
+let out_nn () = E.out_length !O.names
+
+let out_ns () = E.out_uris !O.names
+
let out_oc () = E.out_int !O.net
let out_on () = E.out_length !O.objs
let help_f = " Print the number of objects grouped by flavour" in
let help_g = " Exclude generated objects" in
let help_i = " Exclude implied objects" in
+ let help_nn = " Print the number of names" in
+ let help_ns = " Print the list of names" in
let help_oc = " Print the total intrinsic complexity (objects)" in
let help_on = " Print the number of objects" in
let help_os = " Print the list of objects" in
"-f" , A.Unit out_f , help_f;
"-g" , A.Unit set_g , help_g;
"-i" , A.Unit set_i , help_i;
+ "-nn", A.Unit out_nn, help_nn;
+ "-ns", A.Unit out_ns, help_ns;
"-oc", A.Unit out_oc, help_oc;
"-on", A.Unit out_on, help_on;
"-os", A.Unit out_os, help_os;
PRB := probe.native
PRB_OPTS := $(XOA_OPTS) -g -i
-ORIG := . ./orig.sh
+ORIG := . ./orig.sh
ORIGS := basic_2/basic_1.orig
CONTRIB := lambdadelta_2B
WWW := ../../../../helm/www/lambdadelta
-TAGS := all xoa orig elim deps top leaf stats tbls odeps trim contrib clean \
+TAGS := all names xoa orig elim deps top leaf stats tbls odeps trim contrib clean \
home up-home
PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1
$(foreach PKG, $(XPACKAGES), $(eval $(call XMAS_TEMPLATE,$(PKG))))
+# names ######################################################################
+
+NAMES = basic_1A basic_2A static_2 basic_2
+
+%/names.txt: %/*/*.ma
+ @echo "PROBE $* -ns"
+ $(H)$(PRB_DIR)/$(PRB) $(PRB_OPTS) $* -ns | sort > $@
+
+names: $(NAMES:%=%/names.txt)
+
# xoa ########################################################################
xoa: $(XOA_CONF)
$(DEP_INPUT): $(MAS) Makefile
@echo " GREP include"
$(H)grep "include \"" $(MAS) > $(DEP_INPUT)
- $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT)
+ $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT)
# dep ########################################################################
$$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): D1 = $$(word 5, $$(C0))
$$(STT_$(1)): D2 = $$(word 7, $$(C0))
- $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l)
+ $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): M1 = $$(word 6, $$(C0))
$$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l)
@printf '%-15s %-46s' 'Statistics for:' $(1)
@printf '\x1B[0m\n'
@printf '\x1B[1;40;35m'
- @printf '%-12s' ''
+ @printf '%-12s' ''
@printf ' %-8s %6i' Chars $$(C2)
@printf ' %-7s %7i' Nodes $$(C3)
@printf ' %-11s' ''
--- /dev/null
+A
+Abbr
+Abst
+abst_dec
+AHead
+ahead_inj_snd
+aplus
+aplus_ahead_simpl
+aplus_asort_le_simpl
+aplus_asort_O_simpl
+aplus_asort_simpl
+aplus_assoc
+aplus_asucc
+aplus_asucc_false
+aplus_gz_ge
+aplus_gz_le
+aplus_inj
+aplus_reg_r
+aplus_sort_O_S_simpl
+aplus_sort_S_S_simpl
+app1
+Appl
+aprem
+aprem_asucc
+aprem_gen_head_O
+aprem_gen_head_S
+aprem_gen_sort
+aprem_repl
+aprem_succ
+aprem_zero
+arity
+arity_abbr
+arity_abst
+arity_appl
+arity_appls_abbr
+arity_appls_appl
+arity_appls_bind
+arity_appls_cast
+arity_aprem
+arity_bind
+arity_cast
+arity_cimp_conf
+arity_fsubst0
+arity_gen_abst
+arity_gen_appl
+arity_gen_appls
+arity_gen_bind
+arity_gen_cast
+arity_gen_cvoid
+arity_gen_cvoid_subst0
+arity_gen_lift
+arity_gen_lref
+arity_gen_sort
+arity_head
+arity_lift
+arity_lift1
+arity_mono
+arity_nf2_inv_all
+arity_repellent
+arity_repl
+arity_sort
+arity_sred_pr2
+arity_sred_pr3
+arity_sred_wcpr0_pr0
+arity_sred_wcpr0_pr1
+arity_subst0
+ASort
+asucc
+asucc_gen_head
+asucc_gen_sort
+asucc_inj
+asucc_repl
+B
+Bind
+bind_dec_not
+binder_dec
+C
+Cast
+cbk
+CHead
+chead_ctail
+cimp
+cimp_bind
+cimp_flat_dx
+cimp_flat_sx
+cimp_getl_conf
+cle
+clear
+clear_bind
+clear_cle
+clear_clear
+clear_ctail
+clear_flat
+clear_gen_all
+clear_gen_bind
+clear_gen_flat
+clear_gen_flat_r
+clear_gen_sort
+clear_getl_trans
+clear_mono
+clear_pc3_trans
+clear_pr2_trans
+clear_pr3_trans
+clear_trans
+clear_wf3_trans
+cle_flt_trans
+cle_head
+clen
+cle_r
+cle_trans_head
+clt
+clt_cong
+clt_head
+clt_thead
+clt_wf_ind
+clt_wf__q_ind
+cnt
+cnt_head
+cnt_lift
+cnt_sort
+CSort
+csuba
+csuba_abst
+csuba_arity
+csuba_arity_rev
+csuba_clear_conf
+csuba_clear_trans
+csuba_drop_abbr
+csuba_drop_abbr_rev
+csuba_drop_abst
+csuba_drop_abst_rev
+csuba_gen_abbr
+csuba_gen_abbr_rev
+csuba_gen_abst
+csuba_gen_abst_rev
+csuba_gen_bind
+csuba_gen_bind_rev
+csuba_gen_flat
+csuba_gen_flat_rev
+csuba_gen_void
+csuba_gen_void_rev
+csuba_getl_abbr
+csuba_getl_abbr_rev
+csuba_getl_abst
+csuba_getl_abst_rev
+csuba_head
+csuba_refl
+csuba_sort
+csuba_void
+csubc
+csubc_abst
+csubc_arity_conf
+csubc_arity_trans
+csubc_clear_conf
+csubc_csuba
+csubc_drop1_conf_rev
+csubc_drop_conf_O
+csubc_drop_conf_rev
+csubc_gen_head_l
+csubc_gen_head_r
+csubc_gen_sort_l
+csubc_gen_sort_r
+csubc_getl_conf
+csubc_head
+csubc_refl
+csubc_sort
+csubc_void
+csubst0
+csubst0_both
+csubst0_both_bind
+csubst0_clear_O
+csubst0_clear_O_back
+csubst0_clear_S
+csubst0_clear_trans
+csubst0_drop_eq
+csubst0_drop_eq_back
+csubst0_drop_gt
+csubst0_drop_gt_back
+csubst0_drop_lt
+csubst0_drop_lt_back
+csubst0_fst
+csubst0_fst_bind
+csubst0_gen_head
+csubst0_gen_S_bind_2
+csubst0_gen_sort
+csubst0_getl_ge
+csubst0_getl_ge_back
+csubst0_getl_lt
+csubst0_getl_lt_back
+csubst0_snd
+csubst0_snd_bind
+csubst1
+csubst1_bind
+csubst1_flat
+csubst1_gen_head
+csubst1_getl_ge
+csubst1_getl_ge_back
+csubst1_getl_lt
+csubst1_head
+csubst1_refl
+csubst1_sing
+csubt
+csubt_abst
+csubt_clear_conf
+csubt_csuba
+csubt_drop_abbr
+csubt_drop_abst
+csubt_drop_flat
+csubt_gen_abbr
+csubt_gen_abst
+csubt_gen_bind
+csubt_gen_flat
+csubt_getl_abbr
+csubt_getl_abst
+csubt_head
+csubt_pc3
+csubt_pr2
+csubt_refl
+csubt_sort
+csubt_ty3
+csubt_ty3_ld
+csubt_void
+csubv
+csubv_bind
+csubv_bind_same
+csubv_clear_conf
+csubv_clear_conf_void
+csubv_drop_conf
+csubv_flat
+csubv_getl_conf
+csubv_getl_conf_void
+csubv_refl
+csubv_sort
+csubv_void
+CTail
+c_tail_ind
+cweight
+dnf_dec
+dnf_dec2
+drop
+drop1
+drop1_cons
+drop1_cons_tail
+drop1_csubc_trans
+drop1_gen_pcons
+drop1_gen_pnil
+drop1_getl_trans
+drop1_nil
+drop1_skip_bind
+drop1_trans
+drop_clear
+drop_clear_O
+drop_clear_S
+drop_conf_ge
+drop_conf_lt
+drop_conf_rev
+drop_csubc_trans
+drop_ctail
+drop_drop
+drop_gen_drop
+drop_gen_refl
+drop_gen_skip_l
+drop_gen_skip_r
+drop_gen_sort
+drop_getl_trans_ge
+drop_getl_trans_le
+drop_getl_trans_lt
+drop_mono
+drop_refl
+drop_S
+drop_skip
+drop_skip_bind
+drop_skip_flat
+drop_trans_ge
+drop_trans_le
+ex1_arity
+ex1_c
+ex1__leq_sort_SS
+ex1_t
+ex1_ty3
+ex2_arity
+ex2_c
+ex2_nf2
+ex2_t
+F
+Flat
+flt
+flt_arith0
+flt_arith1
+flt_arith2
+flt_shift
+flt_thead_dx
+flt_thead_sx
+flt_trans
+flt_wf_ind
+flt_wf__q_ind
+fsubst0
+fsubst0_both
+fsubst0_fst
+fsubst0_gen_base
+fsubst0_snd
+fweight
+G
+getl
+getl_clear_bind
+getl_clear_conf
+getl_clear_trans
+getl_conf_ge_drop
+getl_conf_le
+getl_csubst1
+getl_ctail
+getl_ctail_clen
+getl_dec
+getl_drop
+getl_drop_conf_ge
+getl_drop_conf_lt
+getl_drop_conf_rev
+getl_drop_trans
+getl_flat
+getl_flt
+getl_gen_2
+getl_gen_all
+getl_gen_bind
+getl_gen_flat
+getl_gen_O
+getl_gen_S
+getl_gen_sort
+getl_gen_tail
+getl_head
+getl_intro
+getl_mono
+getl_refl
+getl_trans
+getl_wf3_trans
+gz
+iso
+iso_flats_flat_bind_false
+iso_flats_lref_bind_false
+iso_gen_head
+iso_gen_lref
+iso_gen_sort
+iso_head
+iso_lref
+iso_refl
+iso_sort
+iso_trans
+K
+leq
+leq_ahead_asucc_false
+leq_ahead_false_1
+leq_ahead_false_2
+leq_asucc
+leq_asucc_false
+leq_eq
+leq_gen_head1
+leq_gen_head2
+leq_gen_sort1
+leq_gen_sort2
+leq_head
+leq_leqz
+leq_refl
+leq_sort
+leq_sym
+leq_trans
+leqz
+leqz_head
+leqz_leq
+leqz_sort
+lift
+lift1
+lift1_bind
+lift1_cons_tail
+lift1_flat
+lift1_free
+lift1_lift1
+lift1_lref
+lift1_sort
+lift1_xhg
+lift_bind
+lift_d
+lift_flat
+lift_free
+lift_free_sym
+lift_gen_bind
+lift_gen_flat
+lift_gen_head
+lift_gen_lift
+lift_gen_lref
+lift_gen_lref_false
+lift_gen_lref_ge
+lift_gen_lref_lt
+lift_gen_sort
+lift_head
+lift_inj
+lift_lref_ge
+lift_lref_gt
+lift_lref_lt
+lift_r
+lifts
+lifts1
+lifts1_cons
+lifts1_flat
+lifts1_nil
+lifts1_xhg
+lifts_inj
+lift_sort
+lifts_tapp
+lift_tle
+lift_tlt_dx
+lift_weight
+lift_weight_add
+lift_weight_add_O
+lift_weight_map
+llt
+llt_head_dx
+llt_head_sx
+llt_repl
+llt_trans
+llt_wf_ind
+llt_wf__q_ind
+lref_map
+lweight
+lweight_repl
+minus_s_s
+mk_G
+next_plus
+next_plus_assoc
+next_plus_gz
+next_plus_lt
+next_plus_next
+nf0_dec
+nf2
+nf2_abst
+nf2_abst_shift
+nf2_appl_lref
+nf2_appls_lref
+nf2_csort_lref
+nf2_dec
+nf2_gen_abbr
+nf2_gen_abst
+nf2_gen_beta
+nf2_gen_cast
+nf2_gen_flat
+nf2_gen_lref
+nf2_gen__nf2_gen_aux
+nf2_gen_void
+nf2_iso_appls_lref
+nf2_lift
+nf2_lift1
+nf2_lref_abst
+nf2_pr3_confluence
+nf2_pr3_unfold
+nf2_sn3
+nf2_sort
+nfs2
+nfs2_tapp
+node_inh
+not_abbr_abst
+not_abbr_void
+not_abst_void
+not_void_abst
+pc1
+pc1_head
+pc1_head_1
+pc1_head_2
+pc1_pr0_r
+pc1_pr0_u
+pc1_pr0_u2
+pc1_pr0_x
+pc1_refl
+pc1_s
+pc1_t
+pc3
+pc3_abst_dec
+pc3_dec
+pc3_eta
+pc3_fsubst0
+pc3_gen_abst
+pc3_gen_abst_shift
+pc3_gen_appls_lref_abst
+pc3_gen_appls_lref_sort
+pc3_gen_appls_sort_abst
+pc3_gen_cabbr
+pc3_gen_lift
+pc3_gen_lift_abst
+pc3_gen_not_abst
+pc3_gen_sort
+pc3_gen_sort_abst
+pc3_head_1
+pc3_head_12
+pc3_head_2
+pc3_head_21
+pc3_ind_left
+pc3_ind_left__pc3_left_pc3
+pc3_ind_left__pc3_left_pr3
+pc3_ind_left__pc3_left_sym
+pc3_ind_left__pc3_left_trans
+pc3_ind_left__pc3_pc3_left
+pc3_left
+pc3_left_r
+pc3_left_ur
+pc3_left_ux
+pc3_lift
+pc3_nf2
+pc3_nf2_unfold
+pc3_pc1
+pc3_pr0_pr2_t
+pc3_pr2_fsubst0
+pc3_pr2_fsubst0_back
+pc3_pr2_pr2_t
+pc3_pr2_pr3_t
+pc3_pr2_r
+pc3_pr2_u
+pc3_pr2_u2
+pc3_pr2_x
+pc3_pr3_conf
+pc3_pr3_pc3_t
+pc3_pr3_r
+pc3_pr3_t
+pc3_pr3_x
+pc3_refl
+pc3_s
+pc3_t
+pc3_thin_dx
+pc3_wcpr0
+pc3_wcpr0__pc3_wcpr0_t_aux
+pc3_wcpr0_t
+pr0
+pr0_beta
+pr0_comp
+pr0_confluence
+pr0_confluence__pr0_cong_delta
+pr0_confluence__pr0_cong_upsilon_cong
+pr0_confluence__pr0_cong_upsilon_delta
+pr0_confluence__pr0_cong_upsilon_refl
+pr0_confluence__pr0_cong_upsilon_zeta
+pr0_confluence__pr0_delta_delta
+pr0_confluence__pr0_delta_tau
+pr0_confluence__pr0_upsilon_upsilon
+pr0_delta
+pr0_delta1
+pr0_gen_abbr
+pr0_gen_abst
+pr0_gen_appl
+pr0_gen_cast
+pr0_gen_lift
+pr0_gen_lref
+pr0_gen_sort
+pr0_gen_void
+pr0_lift
+pr0_refl
+pr0_subst0
+pr0_subst0_back
+pr0_subst0_fwd
+pr0_subst1
+pr0_subst1_back
+pr0_subst1_fwd
+pr0_tau
+pr0_upsilon
+pr0_zeta
+pr1
+pr1_comp
+pr1_confluence
+pr1_eta
+pr1_head_1
+pr1_head_2
+pr1_pr0
+pr1_refl
+pr1_sing
+pr1_strip
+pr1_t
+pr2
+pr2_cflat
+pr2_change
+pr2_confluence
+pr2_confluence__pr2_delta_delta
+pr2_confluence__pr2_free_delta
+pr2_confluence__pr2_free_free
+pr2_ctail
+pr2_delta
+pr2_delta1
+pr2_free
+pr2_gen_abbr
+pr2_gen_abst
+pr2_gen_appl
+pr2_gen_cabbr
+pr2_gen_cast
+pr2_gen_cbind
+pr2_gen_cflat
+pr2_gen_csort
+pr2_gen_ctail
+pr2_gen_lift
+pr2_gen_lref
+pr2_gen_sort
+pr2_gen_void
+pr2_head_1
+pr2_head_2
+pr2_lift
+pr2_subst1
+pr2_thin_dx
+pr3
+pr3_cflat
+pr3_confluence
+pr3_eta
+pr3_flat
+pr3_gen_abbr
+pr3_gen_abst
+pr3_gen_appl
+pr3_gen_bind
+pr3_gen_cabbr
+pr3_gen_cast
+pr3_gen_lift
+pr3_gen_lref
+pr3_gen_sort
+pr3_gen_void
+pr3_head_1
+pr3_head_12
+pr3_head_2
+pr3_head_21
+pr3_iso_appl_bind
+pr3_iso_appls_abbr
+pr3_iso_appls_appl_bind
+pr3_iso_appls_beta
+pr3_iso_appls_bind
+pr3_iso_appls_cast
+pr3_iso_beta
+pr3_lift
+pr3_pr0_pr2_t
+pr3_pr1
+pr3_pr2
+pr3_pr2_pr2_t
+pr3_pr2_pr3_t
+pr3_pr3_pr3_t
+pr3_refl
+pr3_sing
+pr3_strip
+pr3_subst1
+pr3_t
+pr3_thin_dx
+pr3_wcpr0_t
+ptrans
+r
+r_arith0
+r_arith1
+r_arith2
+r_arith3
+r_arith4
+r_arith5
+r_arith6
+r_arith7
+r_dis
+r_minus
+r_plus
+r_plus_sym
+r_S
+s
+s_arith0
+s_arith1
+sc3
+sc3_abbr
+sc3_abst
+sc3_appl
+sc3_arity
+sc3_arity_csubc
+sc3_arity_gen
+sc3_bind
+sc3_cast
+sc3_lift
+sc3_lift1
+sc3_props__sc3_sn3_abst
+sc3_repl
+sc3_sn3
+s_inc
+s_inj
+s_le
+s_le_gen
+s_lt
+s_lt_gen
+s_minus
+sn3
+sn3_abbr
+sn3_appl_abbr
+sn3_appl_appl
+sn3_appl_appls
+sn3_appl_beta
+sn3_appl_bind
+sn3_appl_cast
+sn3_appl_lref
+sn3_appls_abbr
+sn3_appls_beta
+sn3_appls_bind
+sn3_appls_cast
+sn3_appls_lref
+sn3_beta
+sn3_bind
+sn3_cast
+sn3_cdelta
+sn3_cflat
+sn3_change
+sn3_cpr3_trans
+sn3_gen_bind
+sn3_gen_cflat
+sn3_gen_def
+sn3_gen_flat
+sn3_gen_head
+sn3_gen_lift
+sn3_lift
+sn3_nf2
+sn3_pr2_intro
+sn3_pr3_trans
+sn3_shift
+sn3_sing
+sns3
+sns3_lifts
+sns3_lifts1
+s_plus
+s_plus_sym
+s_r
+s_S
+sty0
+sty0_abbr
+sty0_abst
+sty0_appl
+sty0_bind
+sty0_cast
+sty0_correct
+sty0_gen_appl
+sty0_gen_bind
+sty0_gen_cast
+sty0_gen_lref
+sty0_gen_sort
+sty0_lift
+sty0_sort
+sty1
+sty1_abbr
+sty1_appl
+sty1_bind
+sty1_cast2
+sty1_cnt
+sty1_correct
+sty1_lift
+sty1_sing
+sty1_sty0
+sty1_trans
+subst
+subst0
+subst0_both
+subst0_confluence_eq
+subst0_confluence_lift
+subst0_confluence_neq
+subst0_fst
+subst0_gen_head
+subst0_gen_lift_false
+subst0_gen_lift_ge
+subst0_gen_lift_lt
+subst0_gen_lift_rev_ge
+subst0_gen_lref
+subst0_gen_sort
+subst0_lift_ge
+subst0_lift_ge_s
+subst0_lift_ge_S
+subst0_lift_lt
+subst0_lref
+subst0_refl
+subst0_snd
+subst0_subst0
+subst0_subst0_back
+subst0_tlt
+subst0_tlt_head
+subst0_trans
+subst0_weight_le
+subst0_weight_lt
+subst1
+subst1_confluence_eq
+subst1_confluence_lift
+subst1_confluence_neq
+subst1_ex
+subst1_gen_head
+subst1_gen_lift_eq
+subst1_gen_lift_ge
+subst1_gen_lift_lt
+subst1_gen_lref
+subst1_gen_sort
+subst1_head
+subst1_lift_ge
+subst1_lift_lt
+subst1_lift_S
+subst1_refl
+subst1_single
+subst1_subst1
+subst1_subst1_back
+subst1_trans
+subst_head
+subst_lift_SO
+subst_lref_eq
+subst_lref_gt
+subst_lref_lt
+subst_sort
+subst_subst0
+T
+TApp
+TCons
+tcons_tapp_ex
+term_dec
+terms_props__bind_dec
+terms_props__flat_dec
+terms_props__kind_dec
+THead
+THeads
+theads_tapp
+thead_x_lift_y_y
+thead_x_y_y
+tle
+tle_r
+TList
+tlist_ind_rev
+TLRef
+tlt
+tlt_head_dx
+tlt_head_sx
+tlt_trans
+tlt_wf_ind
+tlt_wf__q_ind
+TNil
+trans
+tslen
+tslt
+tslt_wf_ind
+tslt_wf__q_ind
+TSort
+tweight
+tweight_lt
+ty3
+ty3_abbr
+ty3_abst
+ty3_acyclic
+ty3_appl
+ty3_arity
+ty3_bind
+ty3_cast
+ty3_conv
+ty3_correct
+ty3_cred_pr2
+ty3_cred_pr3
+ty3_csubst0
+ty3_fsubst0
+ty3_gen_abst_abst
+ty3_gen_appl
+ty3_gen_appl_nf2
+ty3_gen_bind
+ty3_gen_cabbr
+ty3_gen_cast
+ty3_gen_cvoid
+ty3_gen_lift
+ty3_gen_lref
+ty3_gen_sort
+ty3_getl_subst0
+ty3_inference
+ty3_inv_appls_lref_nf2
+ty3_inv_lref_lref_nf2
+ty3_inv_lref_nf2
+ty3_inv_lref_nf2_pc3
+ty3_lift
+ty3_nf2_gen__ty3_nf2_inv_abst_aux
+ty3_nf2_inv_abst
+ty3_nf2_inv_abst_premise
+ty3_nf2_inv_abst_premise_csort
+ty3_nf2_inv_all
+ty3_nf2_inv_sort
+ty3_predicative
+ty3_repellent
+ty3_sconv
+ty3_sconv_pc3
+ty3_shift1
+ty3_sn3
+ty3_sort
+ty3_sred_back
+ty3_sred_pr0
+ty3_sred_pr1
+ty3_sred_pr2
+ty3_sred_pr3
+ty3_sred_wcpr0_pr0
+ty3_sty0
+ty3_subst0
+ty3_tred
+ty3_typecheck
+ty3_unique
+tys3
+tys3_cons
+tys3_gen_cons
+tys3_gen_nil
+tys3_nil
+Void
+wadd
+wadd_le
+wadd_lt
+wadd_O
+wcpr0
+wcpr0_comp
+wcpr0_drop
+wcpr0_drop_back
+wcpr0_gen_head
+wcpr0_gen_sort
+wcpr0_getl
+wcpr0_getl_back
+wcpr0_refl
+weight
+weight_add_O
+weight_add_S
+weight_eq
+weight_le
+weight_map
+wf3
+wf3_bind
+wf3_clear_conf
+wf3_flat
+wf3_gen_bind1
+wf3_gen_flat1
+wf3_gen_head2
+wf3_gen_sort1
+wf3_getl_conf
+wf3_idem
+wf3_mono
+wf3_pc3_conf
+wf3_pr2_conf
+wf3_pr3_conf
+wf3_sort
+wf3_total
+wf3_ty3
+wf3_ty3_conf
+wf3_void
-NAMING CONVENTIONS FOR METAVARIABLES
-
-A,B : arity
-C : candidate of reducibility
-D,E : RTM environment
-F,G : global environment
-H : reserved: transient premise
-IH : reserved: inductive premise
-I,J : item
-K,L : local environment
-M,N : reserved: future use
-O :
-P : relocation environment
-Q : elimination predicate
-R : generic predicate/relation
-S : RTM stack
-T,U,V,W: term
-X,Y,Z : reserved: transient objet denoted by a capital letter
-
-a : applicability condition (true = restricted, false = general)
-b : local dropping kind parameter (true = restricted, false = general)
-c : rt-reduction count parameter
-d : term degree
-e : reserved: future use (\lambda\delta 3)
-f,g : local reference transforming map
-h : sort hierarchy parameter
-i,j : local reference depth (de Bruijn's)
-k,l : global reference level
-m,n : iterations
-o : sort degree parameter (origin)
-p,q : binder polarity
-r :
-s : sort index
-t,u :
-v,w : local reference position level (de Bruijn's) (RTM)
-x,y,z : reserved: transient objet denoted by a small letter
-
-NAMING CONVENTIONS FOR CONSTRUCTORS
-
-0: atomic
-2: binary
-
-A: application to vector
-E: empty list
-F: boolean false
-T: boolean true
-
-a: application
-b: generic binder with one argument
-d: abbreviation
-f: generic flat with one argument
-i: generic binder for local environments
-l: typed abstraction
-n: native type annotation
-u: generic binder with zero argument
-x: exclusion
-
-NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
-
-- prefix and first letter
-
-b: bi contex-sensitive for local environments
-c: contex-sensitive for terms
-f: context-freee for closures
-l: sn contex-sensitive for local environments
-r: dx contex-sensitive for local environments
-s: stratified (prefix)
-t: context-free for terms
-
-- second letter
-
-e: reserved for generic entrywise extension
-i: irreducible form
-n: normal form
-p: reflexive parallel transformation
-q: sequential transformation
-r: reducible form
-s: strongly normalizing form
-
-- third letter
-
-b: (q)rst-reduction
-c: conversion
-d: decomposed rt-reduction
-e: decomposed rt-conversion
-g: counted rt-transition (generic)
-m: semi-counted rt-transition (mixed)
-q: restricted reduction
-r: reduction
-s: substitution
-u: supclosure
-w: reserved for generic pointwise extension
-x: uncounted rt-transition (extended)
-y: rt-substitution
-
-- forth letter (if present)
-
-c: proper single step (general) (successor)
-e: reflexive transitive closure to normal form (evaluation)
-g: proper multiple step (general) (greater)
-p: non-reflexive transitive closure (plus)
-q: reflexive closure (question)
-r: proper multiple step (restricted) (restricted)
-s: reflexive transitive closure (star)
-u: proper single step (restricted) (unit)
+aaa_cpm_SO
+aaa_csx
+aaa_fsb
+aaa_ind_csx
+aaa_ind_csx_aux
+aaa_ind_csx_cpxs
+aaa_ind_csx_cpxs_aux
+aaa_ind_fpb
+aaa_ind_fpb_aux
+aaa_ind_fpbg
+aaa_ind_fpbg_aux
+cnr
+cnr_abbr_neg
+cnr_abst
+cnr_appl_simple
+cnr_dec_teqx
+cnr_gref
+cnr_inv_abbr_neg
+cnr_inv_abst
+cnr_inv_appl
+cnr_inv_cast
+cnr_inv_lifts
+cnr_inv_lref_abbr
+cnr_lifts
+cnr_lref_abst
+cnr_lref_atom
+cnr_lref_unit
+cnr_sort
+cnuw
+cnuw_abbr_neg
+cnuw_abst
+cnuw_appl_simple
+cnuw_atom_drops
+cnuw_cpms_trans
+cnuw_ctop
+cnuw_dec
+cnuw_dec_ex
+cnuw_fwd_appl
+cnuw_gref
+cnuw_inv_abbr_pos
+cnuw_inv_cast
+cnuw_inv_lifts
+cnuw_inv_zero_pair
+cnuw_lifts
+cnuw_lref
+cnuw_sort
+cnuw_unit_drops
+cnuw_zero_unit
+cnv
+cnv_acle_omega
+cnv_acle_one
+cnv_acle_trans
+cnv_appl
+cnv_appl_cpes
+cnv_appl_cpts
+cnv_appl_ge
+cnv_appl_ntas_ge
+cnv_bind
+cnv_cast
+cnv_cast_cpes
+cnv_cast_cpts
+cnv_cpcs_dec
+cnv_cpes_dec
+cnv_cpm_conf_lpr_appl_appl_aux
+cnv_cpm_conf_lpr_appl_beta_aux
+cnv_cpm_conf_lpr_appl_theta_aux
+cnv_cpm_conf_lpr_atom_atom_aux
+cnv_cpm_conf_lpr_atom_delta_aux
+cnv_cpm_conf_lpr_atom_ell_aux
+cnv_cpm_conf_lpr_atom_ess_aux
+cnv_cpm_conf_lpr_aux
+cnv_cpm_conf_lpr_beta_beta_aux
+cnv_cpm_conf_lpr_bind_bind_aux
+cnv_cpm_conf_lpr_bind_zeta_aux
+cnv_cpm_conf_lpr_cast_cast_aux
+cnv_cpm_conf_lpr_cast_ee_aux
+cnv_cpm_conf_lpr_cast_epsilon_aux
+cnv_cpm_conf_lpr_delta_delta_aux
+cnv_cpm_conf_lpr_delta_ell_aux
+cnv_cpm_conf_lpr_ee_ee_aux
+cnv_cpm_conf_lpr_epsilon_ee_aux
+cnv_cpm_conf_lpr_epsilon_epsilon_aux
+cnv_cpm_conf_lpr_sub
+cnv_cpm_conf_lpr_theta_theta_aux
+cnv_cpm_conf_lpr_zeta_zeta_aux
+cnv_cpmre_cpms_conf
+cnv_cpmre_mono
+cnv_cpmre_trans
+cnv_cpms_conf
+cnv_cpms_conf_eq
+cnv_cpms_conf_lpr
+cnv_cpms_conf_lpr_aux
+cnv_cpms_conf_lpr_refl_tneqx_sub
+cnv_cpms_conf_lpr_step_tneqx_sub
+cnv_cpms_conf_lpr_teqx_teqx_aux
+cnv_cpms_conf_lpr_teqx_tneqx_aux
+cnv_cpms_conf_lpr_tneqx_tneqx_aux
+cnv_cpms_fwd_appl_sn_decompose
+cnv_cpms_nta
+cnv_cpms_ntas
+cnv_cpms_strip_lpr_sub
+cnv_cpms_teqx_conf_lpr_aux
+cnv_cpms_teqx_strip_lpr_aux
+cnv_cpms_trans
+cnv_cpms_trans_lpr
+cnv_cpms_trans_lpr_sub
+cnv_cpm_teqx_conf_lpr
+cnv_cpm_teqx_conf_lpr_appl_appl_aux
+cnv_cpm_teqx_conf_lpr_atom_atom_aux
+cnv_cpm_teqx_conf_lpr_atom_ess_aux
+cnv_cpm_teqx_conf_lpr_aux
+cnv_cpm_teqx_conf_lpr_bind_bind_aux
+cnv_cpm_teqx_conf_lpr_cast_cast_aux
+cnv_cpm_teqx_cpm_trans_aux
+cnv_cpm_teqx_cpm_trans_sub
+cnv_cpm_trans
+cnv_cpm_trans_lpr
+cnv_cpm_trans_lpr_aux
+cnv_cpmuwe_mono
+cnv_cpmuwe_trans
+cnv_cpr_teqx_fwd_refl
+cnv_dec
+cnv_fpbg_refl_false
+cnv_fqu_conf
+cnv_fqup_conf
+cnv_fquq_conf
+cnv_fqus_conf
+cnv_fwd_aaa
+cnv_fwd_cpms_abst_dx_le
+cnv_fwd_cpm_SO
+cnv_fwd_cpms_total
+cnv_fwd_csx
+cnv_fwd_flat
+cnv_fwd_fsb
+cnv_fwd_pair_sn
+cnv_ind_cpes
+cnv_inv_appl
+cnv_inv_appl_aux
+cnv_inv_appl_cpes
+cnv_inv_appl_cpts
+cnv_inv_appl_ntas
+cnv_inv_bind
+cnv_inv_bind_aux
+cnv_inv_cast
+cnv_inv_cast_aux
+cnv_inv_cast_cpes
+cnv_inv_cast_cpts
+cnv_inv_gref
+cnv_inv_gref_aux
+cnv_inv_lifts
+cnv_inv_lref
+cnv_inv_lref_atom
+cnv_inv_lref_aux
+cnv_inv_lref_drops
+cnv_inv_lref_pair
+cnv_inv_lref_unit
+cnv_inv_zero
+cnv_inv_zero_aux
+cnv_lifts
+cnv_lprs_trans
+cnv_lpr_trans
+cnv_lref
+cnv_lref_drops
+cnv_nta_sn
+cnv_preserve
+cnv_R_cpmuwe_dec
+cnv_R_cpmuwe_total
+cnv_sort
+cnv_zero
+cnx
+cnx_abst
+cnx_appl_simple
+cnx_csx
+cnx_inv_abbr_neg
+cnx_inv_abbr_pos
+cnx_inv_abst
+cnx_inv_appl
+cnx_inv_cast
+cnx_inv_lifts
+cnx_inv_lref_pair
+cnx_lifts
+cnx_lref_atom
+cnx_lref_unit
+cnx_sort
+cnx_teqx_trans
+cpc
+cpc_conf
+cpc_cpcs
+cpc_fwd_cpr
+cpc_refl
+cpcs
+cpcs_aaa_mono
+cpcs_bind1
+cpcs_bind2
+cpcs_bind_dx
+cpcs_bind_sn
+cpcs_canc_dx
+cpcs_canc_sn
+cpcs_cpr_conf
+cpcs_cpr_div
+cpcs_cprs_conf
+cpcs_cprs_div
+cpcs_cprs_dx
+cpcs_cprs_sn
+cpcs_cprs_step_dx
+cpcs_cprs_step_sn
+cpcs_cpr_step_dx
+cpcs_cpr_step_sn
+cpcs_flat
+cpcs_flat_dx_cpr_rev
+cpcs_ind_dx
+cpcs_ind_sn
+cpcs_inv_abst_bi_dx
+cpcs_inv_abst_bi_sn
+cpcs_inv_abst_dx
+cpcs_inv_abst_sn
+cpcs_inv_cprs
+cpcs_inv_lifts_bi
+cpcs_inv_sort_abst
+cpcs_inv_sort_bi
+cpcs_lifts_bi
+cpcs_refl
+cpcs_step_dx
+cpcs_step_sn
+cpcs_strip
+cpcs_sym
+cpcs_trans
+cpc_sym
+cpes
+cpes_aaa_mono
+cpes_cpes_trans
+cpes_cpms_div
+cpes_cprs_trans
+cpes_fwd_abst_bi
+cpes_refl
+cpes_refl_aaa
+cpes_sym
+cpg
+cpg_appl
+cpg_atom
+cpg_beta
+cpg_bind
+cpg_cast
+cpg_cpx
+cpg_delta
+cpg_delta_drops
+cpg_ee
+cpg_ell
+cpg_ell_drops
+cpg_eps
+cpg_ess
+cpg_fwd_bind1_minus
+cpg_inv_abbr1
+cpg_inv_abst1
+cpg_inv_appl1
+cpg_inv_appl1_aux
+cpg_inv_appl1_simple
+cpg_inv_atom1
+cpg_inv_atom1_aux
+cpg_inv_atom1_drops
+cpg_inv_bind1
+cpg_inv_bind1_aux
+cpg_inv_cast1
+cpg_inv_cast1_aux
+cpg_inv_gref1
+cpg_inv_lifts_bi
+cpg_inv_lifts_sn
+cpg_inv_lref1
+cpg_inv_lref1_bind
+cpg_inv_lref1_drops
+cpg_inv_sort1
+cpg_inv_zero1
+cpg_inv_zero1_pair
+cpg_lifts_bi
+cpg_lifts_sn
+cpg_lref
+cpg_refl
+cpg_theta
+cpg_zeta
+cpm
+cpm_aaa_conf
+cpm_appl
+cpm_beta
+cpm_bind
+cpm_bind2
+cpm_bind_unit
+cpm_cast
+cpm_cpms
+cpm_delta
+cpm_delta_drops
+cpm_ee
+cpm_ell
+cpm_ell_drops
+cpm_eps
+cpm_ess
+cpm_fpb
+cpm_fpbq
+cpm_fsge_comp
+cpm_fwd_bind1_minus
+cpm_fwd_cpx
+cpm_fwd_plus
+cpm_fwd_plus_aux
+cpm_ind
+cpm_inv_abbr1
+cpm_inv_abst1
+cpm_inv_abst_bi
+cpm_inv_appl1
+cpm_inv_appl1_simple
+cpm_inv_atom1
+cpm_inv_atom1_drops
+cpm_inv_bind1
+cpm_inv_cast1
+cpm_inv_gref1
+cpm_inv_lifts_bi
+cpm_inv_lifts_sn
+cpm_inv_lref1
+cpm_inv_lref1_ctop
+cpm_inv_lref1_drops
+cpm_inv_sort1
+cpm_inv_zero1
+cpm_inv_zero1_unit
+cpm_lifts_bi
+cpm_lifts_sn
+cpm_lref
+cpmre
+cpmre_fwd_cpms
+cpmre_intro
+cpmre_total_aaa
+cpm_rex_conf
+cpms
+cpms_aaa_conf
+cpms_abst_dx_le_aaa
+cpms_appl
+cpms_appl_dx
+cpms_beta
+cpms_beta_dx
+cpms_beta_rc
+cpms_bind
+cpms_bind2_dx
+cpms_bind_alt
+cpms_bind_dx
+cpms_cast
+cpms_cast_sn
+cpms_cprre_trans
+cpms_cprs_trans
+cpms_delta
+cpms_delta_drops
+cpms_div
+cpms_ee
+cpms_ell
+cpms_ell_drops
+cpms_eps
+cpms_fpbg_trans
+cpms_fwd_cpxs
+cpms_fwd_fpbs
+cpms_ind_dx
+cpms_ind_sn
+cpms_inv_abbr_abst
+cpms_inv_abbr_sn_dx
+cpms_inv_abst_bi
+cpms_inv_abst_sn
+cpms_inv_abst_sn_cprs
+cpms_inv_appl_sn
+cpms_inv_cast1
+cpms_inv_delta_sn
+cpms_inv_ell_sn
+cpms_inv_gref1
+cpms_inv_lifts_bi
+cpms_inv_lifts_sn
+cpms_inv_lref1_ctop
+cpms_inv_lref1_drops
+cpms_inv_lref_sn
+cpms_inv_plus
+cpms_inv_sort1
+cpms_inv_succ_sn
+cpms_inv_zero1_unit
+cpms_lifts_bi
+cpms_lifts_sn
+cpms_lref
+cpm_sort
+cpms_reqx_conf_dx
+cpms_reqx_conf_sn
+cpms_sort
+cpms_step_dx
+cpms_step_sn
+cpms_teqx_ind_sn
+cpms_theta
+cpms_theta_dx
+cpms_theta_rc
+cpms_tneqx_fwd_fpbg
+cpms_tneqx_fwd_step_sn_aux
+cpms_total_aaa
+cpms_trans
+cpms_trans_swap
+cpms_zeta
+cpms_zeta_dx
+cpm_teqx_free
+cpm_teqx_ind
+cpm_teqx_inv_appl_sn
+cpm_teqx_inv_atom_sn
+cpm_teqx_inv_bind_dx
+cpm_teqx_inv_bind_sn
+cpm_teqx_inv_bind_sn_void
+cpm_teqx_inv_cast_sn
+cpm_teqx_inv_lref_sn
+cpm_theta
+cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg
+cpm_tneqx_cpm_fpbg
+cpmuwe
+cpmuwe_abbr_neg
+cpmuwe_abst
+cpmuwe_ctop
+cpmuwe_fwd_cpms
+cpmuwe_gref
+cpmuwe_intro
+cpmuwe_sort
+cpmuwe_total_csx
+cpmuwe_zero_unit
+cpm_zeta
+cpr_abbr_pos_tneqx
+cpr_conf
+cpr_conf_lpr
+cpr_conf_lpr_atom_atom
+cpr_conf_lpr_atom_delta
+cpr_conf_lpr_beta_beta
+cpr_conf_lpr_bind_bind
+cpr_conf_lpr_bind_zeta
+cpr_conf_lpr_delta_delta
+cpr_conf_lpr_eps_eps
+cpr_conf_lpr_flat_beta
+cpr_conf_lpr_flat_eps
+cpr_conf_lpr_flat_flat
+cpr_conf_lpr_flat_theta
+cpr_conf_lpr_theta_theta
+cpr_conf_lpr_zeta_zeta
+cpr_cpcs_dx
+cpr_cpcs_sn
+cpr_cprs_conf_cpcs
+cpr_cprs_div
+cpr_div
+cpr_ext
+cpr_flat
+cpr_ind
+cpr_inv_atom1
+cpr_inv_atom1_drops
+cpr_inv_cast1
+cpr_inv_flat1
+cpr_inv_gref1
+cpr_inv_lref1
+cpr_inv_lref1_drops
+cpr_inv_sort1
+cpr_inv_zero1
+cpr_pair_sn
+cprre_cprs_conf
+cpr_refl
+cprre_mono
+cprre_total_csx
+cprs_abbr_pos_twneq
+cprs_conf
+cprs_conf_cpcs
+cprs_cpr_conf_cpcs
+cprs_cpr_div
+cprs_CTC
+cprs_div
+cprs_ext
+cprs_flat
+cprs_flat_dx
+cprs_flat_sn
+cprs_ind_dx
+cprs_ind_sn
+cprs_inv_appl_sn
+cprs_inv_cast1
+cprs_inv_cnr_sn
+cprs_inv_CTC
+cprs_inv_lref1_drops
+cprs_inv_sort1
+cprs_lpr_conf_dx
+cprs_lpr_conf_sn
+cprs_nta_trans
+cprs_nta_trans_cnv
+cprs_refl
+cprs_step_dx
+cprs_step_sn
+cprs_strip
+cprs_trans
+cpr_subst
+cpt
+cpt_appl
+cpt_bind
+cpt_cast
+cpt_cpts
+cpt_delta
+cpt_delta_drops
+cpt_ee
+cpt_ell
+cpt_ell_drops
+cpt_ess
+cpt_fwd_cpm
+cpt_fwd_plus
+cpt_fwd_plus_aux
+cpt_ind
+cpt_inv_appl_sn
+cpt_inv_atom_sn
+cpt_inv_atom_sn_drops
+cpt_inv_bind_sn
+cpt_inv_cast_sn
+cpt_inv_gref_sn
+cpt_inv_lifts_bi
+cpt_inv_lifts_sn
+cpt_inv_lref_sn
+cpt_inv_lref_sn_ctop
+cpt_inv_lref_sn_drops
+cpt_inv_sort_sn
+cpt_inv_zero_sn
+cpt_inv_zero_sn_unit
+cpt_lifts_bi
+cpt_lifts_sn
+cpt_lref
+cpt_refl
+cpts
+cpts_appl_dx
+cpts_bind_dx
+cpts_cast_sn
+cpts_cpms_conf_eq
+cpts_cprs_trans
+cpts_delta
+cpts_delta_drops
+cpts_ee
+cpts_ell
+cpts_ell_drops
+cpts_fwd_cpms
+cpts_ind_dx
+cpts_ind_sn
+cpts_inv_cast_sn
+cpts_inv_delta_sn
+cpts_inv_ell_sn
+cpts_inv_gref_sn
+cpts_inv_lifts_bi
+cpts_inv_lifts_sn
+cpts_inv_lref_sn
+cpts_inv_lref_sn_ctop
+cpts_inv_lref_sn_drops
+cpts_inv_sort_sn
+cpts_inv_succ_sn
+cpts_inv_zero_sn_unit
+cpts_lifts_bi
+cpts_lifts_sn
+cpts_lref
+cpt_sort
+cpts_refl
+cpts_sort
+cpts_step_dx
+cpts_step_sn
+cpts_total_aaa
+cpx
+cpx_aaa_conf
+cpx_aaa_conf_lpx
+cpx_beta
+cpx_bind
+cpx_bind2
+cpx_bind_unit
+cpx_cpxs
+cpx_delta
+cpx_delta_drops
+cpx_ee
+cpx_eps
+cpx_ess
+cpx_ext
+cpx_flat
+cpx_fsge_comp
+cpx_fwd_bind1_minus
+cpx_ind
+cpx_inv_abbr1
+cpx_inv_abst1
+cpx_inv_appl1
+cpx_inv_appl1_simple
+cpx_inv_atom1
+cpx_inv_atom1_drops
+cpx_inv_bind1
+cpx_inv_cast1
+cpx_inv_flat1
+cpx_inv_gref1
+cpx_inv_lifts_bi
+cpx_inv_lifts_sn
+cpx_inv_lref1
+cpx_inv_lref1_bind
+cpx_inv_lref1_drops
+cpx_inv_sort1
+cpx_inv_zero1
+cpx_inv_zero1_pair
+cpx_lifts_bi
+cpx_lifts_sn
+cpx_lref
+cpx_pair_sn
+cpx_refl
+cpx_req_conf_sn
+cpx_reqx_conf
+cpx_reqx_conf_dx
+cpx_reqx_conf_sn
+cpx_rex_conf
+cpxs
+cpxs_aaa_conf
+cpxs_beta
+cpxs_beta_dx
+cpxs_beta_rc
+cpxs_bind
+cpxs_bind2_dx
+cpxs_bind_alt
+cpxs_bind_dx
+cpxs_cnx
+cpxs_delta
+cpxs_delta_drops
+cpxs_ee
+cpxs_eps
+cpxs_ext
+cpxs_flat
+cpxs_flat_dx
+cpxs_flat_sn
+cpxs_fpbg_trans
+cpxs_fpbs
+cpxs_fpbs_trans
+cpxs_fqup_fpbs
+cpxs_fqus_fpbs
+cpxs_fqus_lpxs_fpbs
+cpxs_fwd_beta
+cpxs_fwd_beta_vector
+cpxs_fwd_cast
+cpxs_fwd_cast_vector
+cpxs_fwd_cnx
+cpxs_fwd_cnx_vector
+cpxs_fwd_delta_drops
+cpxs_fwd_delta_drops_vector
+cpxs_fwd_sort
+cpxs_fwd_sort_vector
+cpxs_fwd_theta
+cpxs_fwd_theta_vector
+cpxs_ind
+cpxs_ind_dx
+cpxs_inv_abbr1_dx
+cpxs_inv_abst1
+cpxs_inv_appl1
+cpxs_inv_cast1
+cpxs_inv_cnx1
+cpxs_inv_lifts_bi
+cpxs_inv_lifts_sn
+cpxs_inv_lref1
+cpxs_inv_lref1_drops
+cpxs_inv_sort1
+cpxs_inv_zero1
+cpxs_lifts_bi
+cpxs_lifts_sn
+cpxs_lref
+cpxs_pair_sn
+cpxs_refl
+cpxs_reqx_conf
+cpxs_reqx_conf_dx
+cpxs_reqx_conf_sn
+cpxs_sort
+cpxs_strap1
+cpxs_strap2
+cpxs_teqx_fpbs
+cpxs_teqx_fpbs_trans
+cpxs_theta
+cpxs_theta_dx
+cpxs_theta_rc
+cpxs_tneqx_fpbg
+cpxs_tneqx_fwd_step_sn
+cpxs_trans
+cpx_subst
+cpxs_zeta
+cpxs_zeta_dx
+cpx_teqx_conf
+cpx_teqx_conf_rex
+cpx_theta
+cpx_zeta
+csx
+csx_abbr
+csx_abst
+csx_appl_beta
+csx_appl_beta_aux
+csx_appl_simple
+csx_appl_simple_teqo
+csx_appl_theta
+csx_appl_theta_aux
+csx_applv_beta
+csx_applv_cast
+csx_applv_cnx
+csx_applv_delta_drops
+csx_applv_sort
+csx_applv_theta
+csx_bind
+csx_cast
+csx_cpcs_dec
+csx_cpxs_trans
+csx_cpx_trans
+csx_feqx_conf
+csx_fpbq_conf
+csx_fqu_conf
+csx_fqup_conf
+csx_fquq_conf
+csx_fqus_conf
+csx_fsb
+csx_fsb_fpbs
+csx_fwd_applv
+csx_fwd_bind
+csx_fwd_bind_dx
+csx_fwd_bind_dx_aux
+csx_fwd_bind_dx_unit
+csx_fwd_bind_dx_unit_aux
+csx_fwd_bind_unit
+csx_fwd_flat
+csx_fwd_flat_dx
+csx_fwd_flat_dx_aux
+csx_fwd_pair_sn
+csx_fwd_pair_sn_aux
+csx_gcp
+csx_gcr
+csx_ind
+csx_ind_cpxs
+csx_ind_cpxs_teqx
+csx_ind_fpb
+csx_ind_fpbg
+csx_intro
+csx_intro_cpxs
+csx_inv_lifts
+csx_inv_lref_drops
+csx_inv_lref_pair_drops
+csx_lifts
+csx_lpx_conf
+csx_lpxs_conf
+csx_lref_pair_drops
+csx_lsubr_conf
+csx_reqx_conf
+csx_reqx_trans
+csx_rsx
+csx_sort
+csx_teqx_trans
+csxv
+csxv_inv_cons
+drops_lprs_trans
+drops_lpr_trans
+drops_lpxs_trans
+drops_lpx_trans
+feqx_cpxs_trans
+feqx_cpx_trans
+feqx_fpbg_trans
+feqx_fpbs
+feqx_fpbs_trans
+feqx_fpb_trans
+feqx_lpxs_trans
+fleq_rpx
+fpb
+fpb_cpx
+fpb_fpbg
+fpb_fpbg_trans
+fpb_fpbq
+fpb_fpbq_fneqx
+fpb_fpbs
+fpb_fqu
+fpbg
+fpbg_cpms_trans
+fpbg_feqx_trans
+fpbg_fpbq_trans
+fpbg_fpbs_trans
+fpbg_fqu_trans
+fpbg_fwd_fpbs
+fpbg_teqx_div
+fpbg_trans
+fpb_inv_feqx
+fpb_lpx
+fpbq
+fpbq_aaa_conf
+fpbq_cpx
+fpbq_feqx
+fpbq_fneqx_inv_fpb
+fpbq_fpbg_trans
+fpbq_fpbs
+fpbq_fquq
+fpbq_inv_fpb
+fpbq_lpx
+fpbq_refl
+fpbs
+fpbs_aaa_conf
+fpbs_cpxs_teqx_fqup_lpx_trans
+fpbs_cpxs_trans
+fpbs_cpx_tneqx_trans
+fpbs_csx_conf
+fpbs_feqx_trans
+fpbs_fpbg_trans
+fpbs_fpb_trans
+fpbs_fqup_trans
+fpbs_fqus_trans
+fpbs_ind
+fpbs_ind_dx
+fpbs_intro_star
+fpbs_inv_fpbg
+fpbs_inv_star
+fpbs_lpxs_trans
+fpbs_lpx_trans
+fpbs_refl
+fpbs_strap1
+fpbs_strap2
+fpbs_teqx_trans
+fpbs_trans
+fqu_cpr_trans_dx
+fqu_cpr_trans_sn
+fqu_cpxs_trans
+fqu_cpxs_trans_tneqx
+fqu_cpx_trans
+fqu_cpx_trans_tneqx
+fqu_lpr_trans
+fqu_lpx_trans
+fqup_cpms_fwd_fpbg
+fqup_cpxs_trans
+fqup_cpxs_trans_tneqx
+fqup_cpx_trans
+fqup_cpx_trans_tneqx
+fqup_fpbg
+fqup_fpbg_trans
+fqup_fpbs
+fqup_fpbs_trans
+fquq_cpr_trans_dx
+fquq_cpr_trans_sn
+fquq_cpxs_trans
+fquq_cpxs_trans_tneqx
+fquq_cpx_trans
+fquq_cpx_trans_tneqx
+fquq_lpr_trans
+fquq_lpx_trans
+fqus_cpxs_trans
+fqus_cpxs_trans_tneqx
+fqus_cpx_trans
+fqus_cpx_trans_tneqx
+fqus_fpbs
+fqus_fpbs_trans
+fqus_lpxs_fpbs
+fsb
+fsb_feqx_trans
+fsb_fpbg_refl_false
+fsb_fpbs_trans
+fsb_ind_alt
+fsb_ind_fpbg
+fsb_ind_fpbg_fpbs
+fsb_intro
+fsb_intro_fpbg
+fsb_inv_csx
+IH_cnv_cpm_conf_lpr
+IH_cnv_cpms_conf_lpr
+IH_cnv_cpms_strip_lpr
+IH_cnv_cpms_trans_lpr
+IH_cnv_cpm_teqx_conf_lpr
+IH_cnv_cpm_teqx_cpm_trans
+IH_cnv_cpm_trans_lpr
+IH_cpr_conf_lpr
+jsx
+jsx_atom
+jsx_bind
+jsx_csx_conf
+jsx_fwd_bind_sn
+jsx_fwd_drops_atom_sn
+jsx_fwd_drops_pair_sn
+jsx_fwd_drops_unit_sn
+jsx_fwd_lsubr
+jsx_inv_atom_sn
+jsx_inv_atom_sn_aux
+jsx_inv_bind_sn
+jsx_inv_bind_sn_aux
+jsx_inv_pair_sn
+jsx_inv_void_sn
+jsx_pair
+jsx_refl
+jsx_trans
+lfsx_atom
+lpr
+lpr_aaa_conf
+lpr_bind
+lpr_bind_refl_dx
+lpr_conf
+lpr_cpcs_conf
+lpr_cpcs_trans
+lpr_cpms_trans
+lpr_cpm_trans
+lpr_cpr_conf
+lpr_cpr_conf_dx
+lpr_cpr_conf_sn
+lpr_cprs_conf
+lpr_cprs_trans
+lpr_cpr_trans
+lpr_drops_conf
+lpr_drops_trans
+lpr_fpb
+lpr_fpbq
+lpr_fquq_trans
+lpr_fqu_trans
+lpr_fwd_length
+lpr_fwd_lpx
+lpr_inv_atom_dx
+lpr_inv_atom_sn
+lpr_inv_bind_dx
+lpr_inv_bind_sn
+lpr_inv_pair
+lpr_inv_pair_dx
+lpr_inv_pair_sn
+lpr_inv_unit_dx
+lpr_inv_unit_sn
+lpr_lprs
+lpr_pair
+lpr_refl
+lprs
+lprs_aaa_conf
+lprs_bind_refl_dx
+lprs_conf
+lprs_cpcs_trans
+lprs_cpms_trans
+lprs_cpm_trans
+lprs_cpr_conf_dx
+lprs_cpr_conf_sn
+lprs_cprs_conf
+lprs_cprs_conf_dx
+lprs_cprs_conf_sn
+lprs_CTC
+lprs_drops_conf
+lprs_drops_trans
+lprs_fwd_length
+lprs_fwd_lpxs
+lprs_ind
+lprs_ind_dx
+lprs_ind_sn
+lprs_inv_atom_dx
+lprs_inv_atom_sn
+lprs_inv_CTC
+lprs_inv_pair_dx
+lprs_inv_pair_sn
+lprs_inv_TC
+lprs_pair
+lprs_pair_dx
+lprs_refl
+lprs_step_dx
+lprs_step_sn
+lprs_strip
+lprs_TC
+lprs_trans
+lpx
+lpx_aaa_conf
+lpx_bind
+lpx_bind_refl_dx
+lpx_cpx_conf_fsge
+lpx_cpxs_trans
+lpx_cpx_trans
+lpx_drops_conf
+lpx_drops_trans
+lpx_fqup_trans
+lpx_fquq_trans
+lpx_fqus_trans
+lpx_fqu_trans
+lpx_fsge_comp
+lpx_fwd_length
+lpx_inv_atom_dx
+lpx_inv_atom_sn
+lpx_inv_bind_dx
+lpx_inv_bind_sn
+lpx_inv_pair
+lpx_inv_pair_dx
+lpx_inv_pair_sn
+lpx_inv_unit_dx
+lpx_inv_unit_sn
+lpx_lpxs
+lpx_pair
+lpx_refl
+lpx_rpx
+lpxs
+lpxs_aaa_conf
+lpxs_bind_refl_dx
+lpxs_cpxs_trans
+lpxs_cpx_trans
+lpxs_drops_conf
+lpxs_drops_trans
+lpxs_feqx_fpbs
+lpxs_fpbs
+lpxs_fpbs_trans
+lpxs_fwd_length
+lpxs_ind
+lpxs_ind_dx
+lpxs_ind_sn
+lpxs_inv_atom_dx
+lpxs_inv_atom_sn
+lpxs_inv_bind_sn
+lpxs_inv_pair_dx
+lpxs_inv_pair_sn
+lpxs_pair
+lpxs_pair_dx
+lpxs_refl
+lpxs_rneqx_fpbg
+lpxs_rneqx_inv_step_sn
+lpxs_step_dx
+lpxs_step_sn
+lpxs_trans
+lsubr_cpcs_trans
+lsubr_cpg_trans
+lsubr_cpms_trans
+lsubr_cpm_trans
+lsubr_cpxs_trans
+lsubr_cpx_trans
+lsubsv_fwd_lsuba
+lsubv
+lsubv_atom
+lsubv_beta
+lsubv_bind
+lsubv_cnv_trans
+lsubv_cpcs_trans
+lsubv_cpms_trans
+lsubv_drops_conf_isuni
+lsubv_drops_trans_isuni
+lsubv_fwd_lsubr
+lsubv_inv_abst_sn
+lsubv_inv_atom_dx
+lsubv_inv_atom_dx_aux
+lsubv_inv_atom_sn
+lsubv_inv_atom_sn_aux
+lsubv_inv_bind_dx
+lsubv_inv_bind_dx_aux
+lsubv_inv_bind_sn
+lsubv_inv_bind_sn_aux
+lsubv_refl
+lsubv_trans
+nta
+nta_abst_predicative
+nta_abst_repellent
+nta_appl
+nta_appl_abst
+nta_appl_ntas_pos
+nta_appl_ntas_zero
+nta_bind_cnv
+nta_cast
+nta_cast_old
+nta_conv
+nta_conv_cnv
+nta_cpcs_bi
+nta_cpcs_conf
+nta_cpcs_conf_cnv
+nta_cpr_conf
+nta_cpr_conf_lpr
+nta_cprs_conf
+nta_cprs_trans
+nta_fwd_aaa
+nta_fwd_cnv_dx
+nta_fwd_cnv_sn
+nta_fwd_correct
+nta_fwd_fsb
+nta_ind_cnv
+nta_ind_ext_cnv
+nta_ind_ext_cnv_mixed
+nta_ind_rest_cnv
+nta_inference_dec
+nta_inv_abst_bi_cnv
+nta_inv_appl_sn
+nta_inv_appl_sn_ntas
+nta_inv_bind_sn_cnv
+nta_inv_cast_sn
+nta_inv_cast_sn_old
+nta_inv_gref_sn
+nta_inv_ldec_sn_cnv
+nta_inv_ldef_sn
+nta_inv_lifts_sn
+nta_inv_lref_sn
+nta_inv_lref_sn_drops_cnv
+nta_inv_pure_sn_cnv
+nta_inv_sort_sn
+nta_ldec_cnv
+nta_ldec_drops_cnv
+nta_ldef
+nta_ldef_drops
+nta_lifts_bi
+nta_lifts_sn
+nta_lpr_conf
+nta_lprs_conf
+nta_lref
+nta_mono
+nta_ntas
+nta_pure_cnv
+ntas
+ntas_bind_cnv
+ntas_fwd_cnv_dx
+ntas_fwd_cnv_sn
+ntas_ind_bi_nta
+ntas_intro
+ntas_inv_appl_sn
+ntas_inv_nta
+ntas_inv_plus
+ntas_inv_zero
+nta_sort
+ntas_refl
+ntas_sort
+ntas_step_dx
+ntas_step_sn
+ntas_trans
+ntas_zero
+nta_typecheck
+nta_typecheck_dec
+R_cpmuwe
+R_cpmuwe_total_csx
+req_cpx_trans
+reqx_cpxs_trans
+reqx_cpx_trans
+reqx_fpb_trans
+reqx_lpxs_trans
+reqx_lpx_trans
+reqx_rpx_trans
+rpr_fsge_comp
+rpx
+rpx_atom
+rpx_bind
+rpx_bind_dx_split
+rpx_bind_dx_split_void
+rpx_bind_repl_dx
+rpx_bind_void
+rpx_cpx_conf
+rpx_cpx_conf_fsge
+rpx_cpx_conf_fsge_dx
+rpx_flat
+rpx_flat_dx_split
+rpx_fsge_comp
+rpx_fwd_bind_dx
+rpx_fwd_bind_dx_void
+rpx_fwd_flat_dx
+rpx_fwd_length
+rpx_fwd_pair_sn
+rpx_gref
+rpx_inv_atom_dx
+rpx_inv_atom_sn
+rpx_inv_bind
+rpx_inv_bind_void
+rpx_inv_flat
+rpx_inv_gref
+rpx_inv_gref_bind_dx
+rpx_inv_gref_bind_sn
+rpx_inv_lifts_bi
+rpx_inv_lifts_dx
+rpx_inv_lifts_sn
+rpx_inv_lpx_req
+rpx_inv_lref
+rpx_inv_lref_bind_dx
+rpx_inv_lref_bind_sn
+rpx_inv_sort
+rpx_inv_sort_bind_dx
+rpx_inv_sort_bind_sn
+rpx_inv_zero_length
+rpx_inv_zero_pair_dx
+rpx_inv_zero_pair_sn
+rpx_lifts_sn
+rpx_lref
+rpx_pair
+rpx_pair_refl
+rpx_pair_sn_split
+rpx_refl
+rpx_reqx_conf
+rpx_sort
+rpx_teqx_conf
+rpx_teqx_div
+rsx
+rsx_bind
+rsx_bind_lpxs_aux
+rsx_bind_lpxs_void_aux
+rsx_bind_void
+rsx_cpxs_trans
+rsx_cpx_trans
+rsx_cpx_trans_jsx
+rsx_flat
+rsx_flat_lpxs
+rsx_fwd_bind_dx_void
+rsx_fwd_flat_dx
+rsx_fwd_lref_pair_csx
+rsx_fwd_lref_pair_csx_aux
+rsx_fwd_lref_pair_csx_drops
+rsx_fwd_lref_pair_drops
+rsx_fwd_pair
+rsx_fwd_pair_aux
+rsx_fwd_pair_sn
+rsx_gref
+rsx_ind
+rsx_ind_lpxs
+rsx_ind_lpxs_reqx
+rsx_intro
+rsx_intro_lpxs
+rsx_inv_bind_void
+rsx_inv_flat
+rsx_inv_lifts
+rsx_inv_lref_drops
+rsx_inv_lref_pair
+rsx_inv_lref_pair_drops
+rsx_jsx_trans
+rsx_lifts
+rsx_lpxs_trans
+rsx_lpx_trans
+rsx_lref_atom_drops
+rsx_lref_pair
+rsx_lref_pair_drops
+rsx_lref_pair_lpxs
+rsx_lref_unit_drops
+rsx_reqx_trans
+rsx_sort
+rsx_unit
+teqx_cpxs_trans
+teqx_cpx_trans
+teqx_fpbs_trans
+teqx_fpb_trans
+teqx_reqx_lpx_fpbs
/3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
(* Basic_2A1: includes cprs_bind2 *)
-lemma cpms_bind_dx (h) (n) (G) (L):
+lemma cpms_bind_alt (h) (n) (G) (L):
∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 →
∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ➡*[h,n] T2 →
∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.
(* Properties with context-sensitive extended rt-computation for terms ******)
(* Basic_2A1: was: cpxs_bind2 *)
-lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 →
- ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ⬈*[h] T2 →
- ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈*[h] ⓑ[p,I]V2.T2.
+lemma cpxs_bind_alt (h) (G):
+ ∀L,V1,V2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 →
+ ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ⬈*[h] T2 →
+ ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈*[h] ⓑ[p,I]V2.T2.
/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
(* Inversion lemmas with context-sensitive ext rt-computation for terms *****)
-lemma cpxs_inv_abst1 (h) (G): ∀p,L,V1,T1,U2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ⬈*[h] U2 →
- ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ⬈*[h] T2 &
- U2 = ⓛ[p]V2.T2.
+lemma cpxs_inv_abst1 (h) (G):
+ ∀p,L,V1,T1,U2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ⬈*[h] U2 →
+ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ⬈*[h] T2 & U2 = ⓛ[p]V2.T2.
#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
(* Basic_2A1: was: cpxs_inv_abbr1 *)
lemma cpxs_inv_abbr1_dx (h) (p) (G) (L):
- ∀V1,T1,U2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ⬈*[h] U2 →
- ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 &
- U2 = ⓓ[p]V2.T2
- | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ.
+ ∀V1,T1,U2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ⬈*[h] U2 →
+ ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈*[h] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & U2 = ⓓ[p]V2.T2
+ | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ⬈*[h] T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ.
#h #p #G #L #V1 #T1 #U2 #H
@(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *
(* Advanced inversion lemmas ************************************************)
(* Note: there must be a proof suitable for lfpr *)
-lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
- ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
+lemma cpcs_inv_abst_bi_sn (h) (G) (L):
+ ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
+ ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
#h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H
elim (cpcs_inv_cprs … H) -H #T #H1 #H2
elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
qed-.
-lemma cpcs_inv_abst_dx (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
- ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW2❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
+lemma cpcs_inv_abst_bi_dx (h) (G) (L):
+ ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
+ ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW2❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
#h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
-#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
+#HT12 elim (cpcs_inv_abst_bi_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
qed-.
] *
#cV #L #W #W2 #HKL #HW2 #HWV2 #H destruct
lapply (lifts_trans … HWV2 … HVT2 ??) -V2 [3,6: |*: // ] #H
- lapply (lifts_uni … H) -H #H
+(* lapply (lifts_uni … H) -H #H *) (**)
/4 width=8 by drops_drop, ex4_4_intro, or3_intro2, or3_intro1/
]
qed-.
]
qed-.
-lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥.
+lemma discr_apair_xy_y: ∀B,A. ②B. A = A → ⊥.
#B #A elim A -A
[ #H destruct
| #Y #X #_ #IHX #H elim (destruct_apair_apair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
--- /dev/null
+aaa
+aaa_abbr
+aaa_abst
+aaa_appl
+aaa_cast
+aaa_csx
+aaa_da
+aaa_fqu_conf
+aaa_fqup_conf
+aaa_fquq_conf
+aaa_fqus_conf
+aaa_fsb
+aaa_fsba
+aaa_ind_csx
+aaa_ind_csx_alt
+aaa_ind_csx_alt_aux
+aaa_ind_csx_aux
+aaa_ind_fpb
+aaa_ind_fpb_aux
+aaa_ind_fpbg
+aaa_ind_fpbg_aux
+aaa_inv_abbr
+aaa_inv_abbr_aux
+aaa_inv_abst
+aaa_inv_abst_aux
+aaa_inv_appl
+aaa_inv_appl_aux
+aaa_inv_cast
+aaa_inv_cast_aux
+aaa_inv_gref
+aaa_inv_gref_aux
+aaa_inv_lift
+aaa_inv_lref
+aaa_inv_lref_aux
+aaa_inv_sort
+aaa_inv_sort_aux
+aaa_lift
+aaa_lifts
+aaa_lleq_conf
+aaa_lref
+aaa_lstas
+aaa_mono
+aaa_sort
+aarity
+AAtom
+Abbr
+Abst
+acr
+acr_aaa
+acr_aaa_csubc_lifts
+acr_abst
+acr_gcr
+APair
+append
+append_assoc
+append_atom_sn
+append_inj_dx
+append_inj_sn
+append_inv_pair_dx
+append_inv_refl_dx
+append_length
+Appl
+ApplDelta
+ApplDelta_lift
+ApplOmega1
+ApplOmega2
+ApplOmega3
+applv
+applv_simple
+at
+at_ge
+at_inv_cons
+at_inv_cons_aux
+at_inv_cons_ge
+at_inv_cons_lt
+at_inv_nil
+at_inv_nil_aux
+at_lt
+at_mono
+at_nil
+bind2
+Bind2
+candidate
+Cast
+ceq
+cfun
+cir
+cir_appl
+cir_cnr
+cir_gref
+cir_ib2
+cir_inv_appl
+cir_inv_bind
+cir_inv_delta
+cir_inv_flat
+cir_inv_ib2
+cir_inv_lift
+cir_inv_ri2
+cir_lift
+cir_sort
+cix
+cix_appl
+cix_cnx
+cix_gref
+cix_ib2
+cix_inv_appl
+cix_inv_bind
+cix_inv_cir
+cix_inv_delta
+cix_inv_flat
+cix_inv_ib2
+cix_inv_lift
+cix_inv_ri2
+cix_inv_sort
+cix_lift
+cix_lref
+cix_sort
+cnr
+cnr_abst
+cnr_appl_simple
+cnr_dec
+cnr_inv_abbr
+cnr_inv_abst
+cnr_inv_appl
+cnr_inv_cir
+cnr_inv_crr
+cnr_inv_delta
+cnr_inv_eps
+cnr_inv_lift
+cnr_inv_zeta
+cnr_lift
+cnr_lref_abst
+cnr_lref_atom
+cnr_lref_free
+cnr_sort
+cnx
+cnx_abst
+cnx_appl_simple
+cnx_csx
+cnx_dec
+cnx_fwd_cnr
+cnx_inv_abbr
+cnx_inv_abst
+cnx_inv_appl
+cnx_inv_cix
+cnx_inv_crx
+cnx_inv_delta
+cnx_inv_eps
+cnx_inv_lift
+cnx_inv_sort
+cnx_inv_zeta
+cnx_lift
+cnx_lref_atom
+cnx_lref_free
+cnx_sort
+cnx_sort_iter
+CP0
+CP1
+CP2
+CP3
+cpc
+cpc_conf
+cpc_cpcs
+cpc_fwd_cpr
+cpc_refl
+cpcs
+cpcs_aaa_mono
+cpcs_bind1
+cpcs_bind2
+cpcs_bind_dx
+cpcs_bind_sn
+cpcs_canc_dx
+cpcs_canc_sn
+cpcs_cpr_conf
+cpcs_cpr_div
+cpcs_cprs_conf
+cpcs_cprs_div
+cpcs_cprs_dx
+cpcs_cprs_sn
+cpcs_cprs_strap1
+cpcs_cprs_strap2
+cpcs_cpr_strap1
+cpcs_cpr_strap2
+cpcs_flat
+cpcs_flat_dx_cpr_rev
+cpcs_ind
+cpcs_ind_dx
+cpcs_inv_abst1
+cpcs_inv_abst2
+cpcs_inv_abst_dx
+cpcs_inv_abst_sn
+cpcs_inv_cprs
+cpcs_inv_lift
+cpcs_inv_sort
+cpcs_inv_sort_abst
+cpcs_lift
+cpcs_refl
+cpcs_scpes
+cpcs_strap1
+cpcs_strap2
+cpcs_strip
+cpcs_sym
+cpcs_trans
+cpc_sym
+cpr
+cpr_aaa_conf
+cpr_ApplOmega_12
+cpr_ApplOmega_23
+cpr_atom
+cpr_beta
+cpr_bind
+cpr_bind2
+cpr_conf
+cpr_conf_lpr
+cpr_conf_lpr_atom_atom
+cpr_conf_lpr_atom_delta
+cpr_conf_lpr_beta_beta
+cpr_conf_lpr_bind_bind
+cpr_conf_lpr_bind_zeta
+cpr_conf_lpr_delta_delta
+cpr_conf_lpr_eps_eps
+cpr_conf_lpr_flat_beta
+cpr_conf_lpr_flat_eps
+cpr_conf_lpr_flat_flat
+cpr_conf_lpr_flat_theta
+cpr_conf_lpr_theta_theta
+cpr_conf_lpr_zeta_zeta
+cpr_cpcs_dx
+cpr_cpcs_sn
+cpr_cprs
+cpr_cprs_conf_cpcs
+cpr_cprs_div
+cpr_cpx
+cpr_delift
+cpr_delta
+cpr_div
+cpre
+cpre_mono
+cpr_eps
+cpr_flat
+cpr_fpb
+cpr_fpbq
+cpr_fwd_bind1_minus
+cpr_fwd_cir
+cpr_inv_abbr1
+cpr_inv_abst1
+cpr_inv_appl1
+cpr_inv_appl1_simple
+cpr_inv_atom1
+cpr_inv_atom1_aux
+cpr_inv_bind1
+cpr_inv_bind1_aux
+cpr_inv_cast1
+cpr_inv_flat1
+cpr_inv_flat1_aux
+cpr_inv_gref1
+cpr_inv_lift1
+cpr_inv_lref1
+cpr_inv_sort1
+cpr_lift
+cpr_llpx_sn_conf
+cpr_lpr_fpbs
+cpr_lpr_sta_fpbs
+cpr_Omega_12
+cpr_Omega_21
+cpr_pair_sn
+cpr_refl
+cprs
+cprs_aaa_conf
+cprs_beta
+cprs_beta_dx
+cprs_beta_rc
+cprs_bind
+cprs_bind2
+cprs_bind2_dx
+cprs_bind_dx
+cprs_conf
+cprs_conf_cpcs
+cprs_cpr_conf_cpcs
+cprs_cpr_div
+cprs_cpxs
+cprs_delta
+cprs_div
+cprs_eps
+cprs_flat
+cprs_flat_dx
+cprs_flat_sn
+cprs_fpbs
+cprs_ind
+cprs_ind_dx
+cprs_inv_abbr1
+cprs_inv_abst
+cprs_inv_abst1
+cprs_inv_appl1
+cprs_inv_cast1
+cprs_inv_cnr1
+cprs_inv_lift1
+cprs_inv_lref1
+cprs_inv_sort1
+cprs_lift
+cprs_lpr_conf_dx
+cprs_lpr_conf_sn
+cprs_refl
+cprs_scpds_div
+cprs_strap1
+cprs_strap2
+cprs_strip
+cprs_theta
+cprs_theta_dx
+cprs_theta_rc
+cprs_trans
+cprs_zeta
+cpr_theta
+cpr_zeta
+cpx
+cpx_aaa_conf
+cpx_atom
+cpx_beta
+cpx_bind
+cpx_bind2
+cpx_cpxs
+cpx_ct
+cpx_delift
+cpx_delta
+cpxe
+cpx_eps
+cpx_flat
+cpx_frees_trans
+cpx_fwd_bind1_minus
+cpx_fwd_cix
+cpx_inv_abbr1
+cpx_inv_abst1
+cpx_inv_appl1
+cpx_inv_appl1_simple
+cpx_inv_atom1
+cpx_inv_atom1_aux
+cpx_inv_bind1
+cpx_inv_bind1_aux
+cpx_inv_cast1
+cpx_inv_flat1
+cpx_inv_flat1_aux
+cpx_inv_gref1
+cpx_inv_lift1
+cpx_inv_lref1
+cpx_inv_lref1_ge
+cpx_inv_sort1
+cpx_lift
+cpx_lleq_conf
+cpx_lleq_conf_dx
+cpx_lleq_conf_sn
+cpx_llpx_sn_conf
+cpx_lpx_aaa_conf
+cpx_pair_sn
+cpx_refl
+cpxs
+cpxs_aaa_conf
+cpxs_ApplOmega_13
+cpxs_beta
+cpxs_beta_dx
+cpxs_beta_rc
+cpxs_bind
+cpxs_bind2
+cpxs_bind2_dx
+cpxs_bind_dx
+cpxs_ct
+cpxs_delta
+cpxs_eps
+cpxs_flat
+cpxs_flat_dx
+cpxs_flat_sn
+cpxs_fpbg
+cpxs_fpbs
+cpxs_fpbs_trans
+cpxs_fqup_fpbs
+cpxs_fqus_fpbs
+cpxs_fqus_lpxs_fpbs
+cpxs_fwd_beta
+cpxs_fwd_beta_vector
+cpxs_fwd_cast
+cpxs_fwd_cast_vector
+cpxs_fwd_cnx
+cpxs_fwd_cnx_vector
+cpxs_fwd_delta
+cpxs_fwd_delta_vector
+cpxs_fwd_sort
+cpxs_fwd_sort_vector
+cpxs_fwd_theta
+cpxs_fwd_theta_vector
+cpxs_ind
+cpxs_ind_dx
+cpxs_inv_abbr1
+cpxs_inv_abst1
+cpxs_inv_appl1
+cpxs_inv_cast1
+cpxs_inv_cnx1
+cpxs_inv_lift1
+cpxs_inv_lref1
+cpxs_inv_sort1
+cpxs_lift
+cpxs_lleq_conf
+cpxs_lleq_conf_dx
+cpxs_lleq_conf_sn
+cpxs_neq_inv_step_sn
+cpxs_pair_sn
+cpxs_refl
+cpxs_sort
+cpxs_strap1
+cpxs_strap2
+cpx_st
+cpxs_theta
+cpxs_theta_dx
+cpxs_theta_rc
+cpxs_trans
+cpxs_zeta
+cpx_theta
+cpx_zeta
+cpy
+cpy_atom
+cpy_bind
+cpy_conf_eq
+cpy_conf_neq
+cpy_cpys
+cpy_flat
+cpy_full
+cpy_fwd_nlift2_ge
+cpy_fwd_tw
+cpy_fwd_up
+cpy_inv_atom1
+cpy_inv_atom1_aux
+cpy_inv_bind1
+cpy_inv_bind1_aux
+cpy_inv_flat1
+cpy_inv_flat1_aux
+cpy_inv_gref1
+cpy_inv_lift1_be
+cpy_inv_lift1_be_up
+cpy_inv_lift1_eq
+cpy_inv_lift1_ge
+cpy_inv_lift1_ge_up
+cpy_inv_lift1_le
+cpy_inv_lift1_le_up
+cpy_inv_lref1
+cpy_inv_refl_O2
+cpy_inv_refl_O2_aux
+cpy_inv_sort1
+cpy_lift_be
+cpy_lift_ge
+cpy_lift_le
+cpy_refl
+cpys
+cpysa
+cpysa_atom
+cpysa_bind
+cpysa_cpy_trans
+cpysa_flat
+cpysa_inv_cpys
+cpys_antisym_eq
+cpysa_refl
+cpysa_subst
+cpys_bind
+cpys_conf_eq
+cpys_conf_neq
+cpys_cpysa
+cpys_flat
+cpys_fwd_tw
+cpys_fwd_up
+cpys_ind
+cpys_ind_alt
+cpys_ind_dx
+cpys_inv_atom1
+cpys_inv_bind1
+cpys_inv_flat1
+cpys_inv_gref1
+cpys_inv_lift1_be
+cpys_inv_lift1_be_up
+cpys_inv_lift1_eq
+cpys_inv_lift1_ge
+cpys_inv_lift1_ge_up
+cpys_inv_lift1_le
+cpys_inv_lift1_le_up
+cpys_inv_lift1_subst
+cpys_inv_lift1_up
+cpys_inv_lref1
+cpys_inv_lref1_drop
+cpys_inv_lref1_Y2
+cpys_inv_refl_O2
+cpys_inv_SO2
+cpys_inv_sort1
+cpys_lift_be
+cpys_lift_ge
+cpys_lift_le
+cpy_split_down
+cpy_split_up
+cpys_refl
+cpys_split_up
+cpys_strap1
+cpys_strap1_down
+cpys_strap2
+cpys_strap2_down
+cpys_strip_eq
+cpys_strip_neq
+cpys_subst
+cpys_subst_Y2
+cpys_trans_down
+cpys_trans_eq
+cpy_subst
+cpys_weak
+cpys_weak_full
+cpys_weak_top
+cpy_trans_down
+cpy_trans_ge
+cpy_weak
+cpy_weak_full
+cpy_weak_top
+crr
+crr_appl_dx
+crr_appl_sn
+crr_beta
+crr_crx
+crr_delta
+crr_ib2_dx
+crr_ib2_sn
+crr_inv_appl
+crr_inv_appl_aux
+crr_inv_gref
+crr_inv_gref_aux
+crr_inv_ib2
+crr_inv_ib2_aux
+crr_inv_lift
+crr_inv_lref
+crr_inv_lref_aux
+crr_inv_sort
+crr_inv_sort_aux
+crr_lift
+crr_ri2
+crr_theta
+crx
+crx_appl_dx
+crx_appl_sn
+crx_beta
+crx_delta
+crx_ib2_dx
+crx_ib2_sn
+crx_inv_appl
+crx_inv_appl_aux
+crx_inv_gref
+crx_inv_gref_aux
+crx_inv_ib2
+crx_inv_ib2_aux
+crx_inv_lift
+crx_inv_lref
+crx_inv_lref_aux
+crx_inv_sort
+crx_inv_sort_aux
+crx_lift
+crx_ri2
+crx_sort
+crx_theta
+csx
+csxa
+csx_abbr
+csx_abst
+csxa_cpxs_trans
+csxa_csx
+csxa_ind
+csxa_intro
+csxa_intro_aux
+csxa_intro_cpx
+csx_appl_beta
+csx_appl_beta_aux
+csx_appl_simple
+csx_appl_simple_tsts
+csx_appl_theta
+csx_appl_theta_aux
+csx_applv_beta
+csx_applv_cast
+csx_applv_cnx
+csx_applv_delta
+csx_applv_sort
+csx_applv_theta
+csx_cast
+csx_cpre
+csx_cpxe
+csx_cpxs_trans
+csx_cpx_trans
+csx_csxa
+csx_fpb_conf
+csx_fpbs_conf
+csx_fqu_conf
+csx_fqup_conf
+csx_fquq_conf
+csx_fqus_conf
+csx_fsb
+csx_fsb_fpbs
+csx_fwd_applv
+csx_fwd_bind
+csx_fwd_bind_dx
+csx_fwd_bind_dx_aux
+csx_fwd_flat
+csx_fwd_flat_dx
+csx_fwd_flat_dx_aux
+csx_fwd_pair_sn
+csx_fwd_pair_sn_aux
+csx_gcp
+csx_gcr
+csx_ind
+csx_ind_alt
+csx_ind_fpb
+csx_ind_fpbg
+csx_intro
+csx_intro_cpxs
+csx_inv_lift
+csx_inv_lref_bind
+csx_lift
+csx_lleq_conf
+csx_lleq_trans
+csx_lpx_conf
+csx_lpxs_conf
+csx_lref_bind
+csx_lsx
+csx_sort
+csxv
+csxv_inv_cons
+d1_liftable_liftables
+d1_liftables_liftables_all
+da
+da_bind
+da_cpr_lpr
+da_cpr_lpr_aux
+da_cprs_lpr
+da_cprs_lpr_aux
+da_flat
+da_inv_bind
+da_inv_bind_aux
+da_inv_flat
+da_inv_flat_aux
+da_inv_gref
+da_inv_gref_aux
+da_inv_lift
+da_inv_lref
+da_inv_lref_aux
+da_inv_sort
+da_inv_sort_aux
+da_ldec
+da_ldef
+da_lift
+da_lstas
+da_mono
+d_appendable_sn
+da_scpds_lpr_aux
+da_scpes_aux
+da_sort
+d_deliftable_sn
+d_deliftable_sn_llstar
+d_deliftable_sn_LTC
+dedropable_sn
+dedropable_sn_TC
+deg_inv_prec
+deg_inv_pred
+deg_iter
+deg_next_SO
+deg_O
+deg_SO
+deg_SO_gt
+deg_SO_inv_pos
+deg_SO_inv_pos_aux
+deg_SO_pos
+deg_SO_refl
+deg_SO_zero
+Delta
+Delta_lift
+destruct_apair_apair_aux
+destruct_lpair_lpair_aux
+destruct_sort_sort_aux
+destruct_tatom_tatom_aux
+destruct_tpair_tpair_aux
+discr_apair_xy_x
+discr_apair_xy_y
+discr_lpair_x_xy
+discr_tpair_xy_x
+discr_tpair_xy_y
+d_liftable
+d_liftable1
+d_liftable_llstar
+d_liftable_LTC
+d_liftables1
+d_liftables1_all
+drop
+dropable_dx
+dropable_dx_TC
+dropable_sn
+dropable_sn_TC
+drop_atom
+drop_conf_be
+drop_conf_div
+drop_conf_ge
+drop_conf_le
+drop_conf_lt
+drop_drop
+drop_drop_lt
+drop_FT
+drop_fwd_be
+drop_fwd_drop2
+drop_fwd_length
+drop_fwd_length_eq1
+drop_fwd_length_eq2
+drop_fwd_length_ge
+drop_fwd_length_le2
+drop_fwd_length_le4
+drop_fwd_length_le_ge
+drop_fwd_length_le_le
+drop_fwd_length_lt2
+drop_fwd_length_lt4
+drop_fwd_length_minus2
+drop_fwd_length_minus4
+drop_fwd_lw
+drop_fwd_lw_lt
+drop_fwd_rfw
+drop_gen
+drop_inv_atom1
+drop_inv_atom1_aux
+drop_inv_drop1
+drop_inv_drop1_lt
+drop_inv_FT
+drop_inv_FT_aux
+drop_inv_gen
+drop_inv_length_eq
+drop_inv_O1_gt
+drop_inv_O1_pair1
+drop_inv_O1_pair1_aux
+drop_inv_O1_pair2
+drop_inv_O2
+drop_inv_O2_aux
+drop_inv_pair1
+drop_inv_refl
+drop_inv_skip1
+drop_inv_skip1_aux
+drop_inv_skip2
+drop_inv_skip2_aux
+drop_inv_T
+drop_lprs_trans
+drop_lpr_trans
+drop_lpxs_trans
+drop_lpx_trans
+drop_lsubc_trans
+drop_mono
+drop_O1_append_sn_le
+drop_O1_append_sn_le_aux
+drop_O1_eq
+drop_O1_ex
+drop_O1_ge
+drop_O1_inj
+drop_O1_inv_append1_ge
+drop_O1_inv_append1_le
+drop_O1_le
+drop_O1_lt
+drop_O1_pair
+drop_pair
+drop_refl
+drop_refl_atom_O2
+drops
+drops_cons
+drops_drop_trans
+drops_inv_cons
+drops_inv_cons_aux
+drops_inv_nil
+drops_inv_nil_aux
+drops_inv_skip2
+drop_skip
+drop_skip_lt
+drops_lsubc_trans
+drops_nil
+drop_split
+drops_skip
+drops_trans
+drop_T
+drop_trans_ge
+drop_trans_ge_comm
+drop_trans_le
+drop_trans_lt
+eq_aarity_dec
+eq_bind2_dec
+eq_false_inv_tpair_dx
+eq_false_inv_tpair_sn
+eq_flat2_dec
+eq_genv_dec
+eq_item0_dec
+eq_item2_dec
+eq_lenv_dec
+eq_term_dec
+flat2
+Flat2
+fleq
+fleq_canc_dx
+fleq_canc_sn
+fleq_fpbg_trans
+fleq_fpbq
+fleq_fpbs
+fleq_fpb_trans
+fleq_intro
+fleq_inv_gen
+fleq_refl
+fleq_sym
+fleq_trans
+fpb
+fpb_cpx
+fpb_fpbg
+fpb_fpbg_trans
+fpb_fpbq
+fpb_fpbq_alt
+fpb_fpbs
+fpb_fpbsa_trans
+fpb_fqu
+fpbg
+fpbg_fleq_trans
+fpbg_fpbq_trans
+fpbg_fpbs_trans
+fpbg_fwd_fpbs
+fpbg_refl
+fpbg_trans
+fpb_inv_fleq
+fpb_lpx
+fpbq
+fpbqa
+fpbq_aaa_conf
+fpbqa_inv_fpbq
+fpbq_cpx
+fpbq_fpbg_trans
+fpbq_fpbqa
+fpbq_fpbs
+fpbq_fquq
+fpbq_ind_alt
+fpbq_inv_fpb_alt
+fpbq_lleq
+fpbq_lpx
+fpbq_refl
+fpbs
+fpbsa
+fpbs_aaa_conf
+fpbsa_inv_fpbs
+fpbs_cpxs_trans
+fpbs_cpx_trans_neq
+fpbs_fpbg
+fpbs_fpbg_trans
+fpbs_fpbsa
+fpbs_fpb_trans
+fpbs_fqup_trans
+fpbs_fqus_trans
+fpbs_ind
+fpbs_ind_dx
+fpbs_intro_alt
+fpbs_inv_alt
+fpbs_lleq_trans
+fpbs_lpxs_trans
+fpbs_refl
+fpbs_strap1
+fpbs_strap2
+fpbs_trans
+fqu
+fqu_bind_dx
+fqu_cpr_trans_dx
+fqu_cpr_trans_sn
+fqu_cpxs_trans
+fqu_cpxs_trans_neq
+fqu_cpx_trans
+fqu_cpx_trans_neq
+fqu_drop
+fqu_drop_lt
+fqu_flat_dx
+fqu_fqup
+fqu_fquq
+fqu_fwd_fw
+fqu_fwd_length_lref1
+fqu_fwd_length_lref1_aux
+fqu_inv_eq
+fqu_inv_eq_aux
+fqu_lpr_trans
+fqu_lpx_trans
+fqu_lref_O
+fqu_lref_S_lt
+fqup
+fqu_pair_sn
+fqup_ApplOmega_13
+fqup_bind_dx
+fqup_bind_dx_flat_dx
+fqup_cpxs_trans
+fqup_cpxs_trans_neq
+fqup_cpx_trans
+fqup_cpx_trans_neq
+fqup_drop
+fqup_flat_dx
+fqup_flat_dx_bind_dx
+fqup_flat_dx_pair_sn
+fqup_fpbg
+fqup_fpbs
+fqup_fqus
+fqup_fqus_trans
+fqup_fwd_fw
+fqup_ind
+fqup_ind_dx
+fqup_inv_step_sn
+fqup_lref
+fqup_pair_sn
+fqup_strap1
+fqup_strap2
+fqup_trans
+fqup_wf_ind
+fqup_wf_ind_eq
+fquq
+fquqa
+fquqa_drop
+fquqa_inv_fquq
+fquqa_refl
+fquq_bind_dx
+fquq_cpr_trans_dx
+fquq_cpr_trans_sn
+fquq_cpxs_trans
+fquq_cpxs_trans_neq
+fquq_cpx_trans
+fquq_cpx_trans_neq
+fquq_drop
+fquq_flat_dx
+fquq_fquqa
+fquq_fqus
+fquq_fwd_fw
+fquq_fwd_length_lref1
+fquq_fwd_length_lref1_aux
+fquq_inv_gen
+fquq_lpr_trans
+fquq_lpx_trans
+fquq_lref_O
+fquq_lstas_trans
+fquq_pair_sn
+fquq_refl
+fquq_sta_trans
+fqus
+fqus_cpxs_trans
+fqus_cpxs_trans_neq
+fqus_cpx_trans
+fqus_cpx_trans_neq
+fqus_drop
+fqus_fpbs
+fqus_fpbs_trans
+fqus_fqup_trans
+fqus_fwd_fw
+fqus_ind
+fqus_ind_dx
+fqus_inv_gen
+fqus_lpxs_fpbs
+fqus_lstas_trans
+fqus_refl
+fqus_strap1
+fqus_strap1_fqu
+fqus_strap2
+fqus_strap2_fqu
+fqu_sta_trans
+fqus_trans
+fqu_wf_ind
+frees
+frees_append
+frees_be
+frees_bind_dx
+frees_bind_dx_O
+frees_bind_sn
+frees_dec
+frees_eq
+frees_flat_dx
+frees_flat_sn
+frees_inv
+frees_inv_append
+frees_inv_append_aux
+frees_inv_bind
+frees_inv_bind_O
+frees_inv_flat
+frees_inv_gref
+frees_inv_lift_be
+frees_inv_lift_ge
+frees_inv_lref
+frees_inv_lref_free
+frees_inv_lref_ge
+frees_inv_lref_lt
+frees_inv_lref_skip
+frees_inv_sort
+frees_lift_ge
+frees_lref_be
+frees_lref_eq
+frees_lreq_conf
+frees_S
+frees_trans
+frees_weak
+fsb
+fsba
+fsba_fpbs_trans
+fsba_ind_alt
+fsba_intro
+fsba_inv_fsb
+fsb_fpbs_trans
+fsb_fsba
+fsb_ind_alt
+fsb_ind_fpbg
+fsb_intro
+fsb_inv_csx
+fw
+fw_lpair_sn
+fw_shift
+fw_tpair_dx
+fw_tpair_sn
+gcp
+gcp0_lifts
+gcp2_lifts
+gcp2_lifts_all
+gcr
+gcr_aaa
+gcr_lift
+gcr_lifts
+genv
+gget
+gget_dec
+gget_eq
+gget_gt
+gget_inv_eq
+gget_inv_gt
+gget_inv_lt
+gget_inv_lt_aux
+gget_lt
+gget_mono
+gget_total
+GRef
+ib2
+IH_da_cpr_lpr
+IH_lstas_cpr_lpr
+IH_snv_cpr_lpr
+IH_snv_lstas
+is_lift_dec
+item0
+item2
+LAtom
+lcosx
+lcosx_drop_trans_lt
+lcosx_inv_pair
+lcosx_inv_succ
+lcosx_inv_succ_aux
+lcosx_O
+lcosx_pair
+lcosx_skip
+lcosx_sort
+length
+length_inv_pos_dx
+length_inv_pos_dx_ltail
+length_inv_pos_sn
+length_inv_pos_sn_ltail
+length_inv_zero_dx
+length_inv_zero_sn
+lenv
+lenv_ind_alt
+lift
+lift_bind
+lift_conf_be
+lift_conf_O1
+lift_div_be
+lift_div_le
+lift_flat
+lift_fwd_pair1
+lift_fwd_pair2
+lift_fwd_tw
+lift_gref
+lift_inj
+lift_inv_bind1
+lift_inv_bind1_aux
+lift_inv_bind2
+lift_inv_bind2_aux
+lift_inv_flat1
+lift_inv_flat1_aux
+lift_inv_flat2
+lift_inv_flat2_aux
+lift_inv_gref1
+lift_inv_gref1_aux
+lift_inv_gref2
+lift_inv_gref2_aux
+lift_inv_lref1
+lift_inv_lref1_aux
+lift_inv_lref1_ge
+lift_inv_lref1_lt
+lift_inv_lref2
+lift_inv_lref2_aux
+lift_inv_lref2_be
+lift_inv_lref2_ge
+lift_inv_lref2_lt
+lift_inv_O2
+lift_inv_O2_aux
+lift_inv_pair_xy_x
+lift_inv_pair_xy_y
+lift_inv_sort1
+lift_inv_sort1_aux
+lift_inv_sort2
+lift_inv_sort2_aux
+lift_lref_ge
+lift_lref_ge_minus
+lift_lref_ge_minus_eq
+lift_lref_lt
+lift_mono
+lift_refl
+lifts
+lifts_applv
+lifts_bind
+lifts_cons
+lifts_flat
+lift_simple_dx
+lift_simple_sn
+lifts_inv_applv1
+lifts_inv_bind1
+lifts_inv_cons
+lifts_inv_cons_aux
+lifts_inv_flat1
+lifts_inv_gref1
+lifts_inv_lref1
+lifts_inv_nil
+lifts_inv_nil_aux
+lifts_inv_sort1
+lifts_lift_trans
+lifts_lift_trans_le
+lifts_nil
+lift_sort
+lift_split
+lifts_simple_dx
+lifts_simple_sn
+lifts_total
+lifts_trans
+liftsv
+liftsv_cons
+liftsv_liftv_trans_le
+liftsv_nil
+lift_total
+lift_trans_be
+lift_trans_ge
+lift_trans_le
+liftv
+liftv_cons
+liftv_inv_cons1
+liftv_inv_cons1_aux
+liftv_inv_nil1
+liftv_inv_nil1_aux
+liftv_mono
+liftv_nil
+liftv_total
+lleq
+lleq_aaa_trans
+lleq_bind
+lleq_bind_O
+lleq_bind_repl_O
+lleq_bind_repl_SO
+lleq_canc_dx
+lleq_canc_sn
+lleq_cpxs_trans
+lleq_cpx_trans
+lleq_dec
+lleq_flat
+lleq_fpbs
+lleq_fpbs_trans
+lleq_fpb_trans
+lleq_fqup_trans
+lleq_fquq_trans
+lleq_fqus_trans
+lleq_fqu_trans
+lleq_free
+lleq_fwd_bind_dx
+lleq_fwd_bind_O_dx
+lleq_fwd_bind_sn
+lleq_fwd_drop_dx
+lleq_fwd_drop_sn
+lleq_fwd_flat_dx
+lleq_fwd_flat_sn
+lleq_fwd_length
+lleq_fwd_lref
+lleq_fwd_lref_dx
+lleq_fwd_lref_sn
+lleq_ge
+lleq_ge_up
+lleq_gref
+lleq_ind
+lleq_ind_alt_r
+lleq_intro_alt
+lleq_intro_alt_r
+lleq_inv_alt
+lleq_inv_alt_r
+lleq_inv_bind
+lleq_inv_bind_O
+lleq_inv_flat
+lleq_inv_lift_be
+lleq_inv_lift_ge
+lleq_inv_lift_le
+lleq_inv_lref_ge
+lleq_inv_lref_ge_bi
+lleq_inv_lref_ge_dx
+lleq_inv_lref_ge_sn
+lleq_inv_S
+lleq_lift_ge
+lleq_lift_le
+lleq_llpx_sn_conf
+lleq_llpx_sn_trans
+lleq_lpxs_trans
+lleq_lpx_trans
+lleq_lref
+lleq_lreq_repl
+lleq_lreq_trans
+lleq_nlleq_trans
+lleq_refl
+lleq_skip
+lleq_sort
+lleq_sym
+lleq_trans
+lleq_transitive
+lleq_Y
+llor
+llor_atom
+llor_skip
+llor_tail_cofrees
+llor_tail_frees
+llor_total
+llpx_sn
+llpx_sn_alt
+llpx_sn_alt_inv_llpx_sn
+llpx_sn_alt_r
+llpx_sn_alt_r_bind
+llpx_sn_alt_r_flat
+llpx_sn_alt_r_free
+llpx_sn_alt_r_fwd_length
+llpx_sn_alt_r_fwd_lref
+llpx_sn_alt_r_gref
+llpx_sn_alt_r_ind_alt
+llpx_sn_alt_r_intro
+llpx_sn_alt_r_intro_alt
+llpx_sn_alt_r_inv_alt
+llpx_sn_alt_r_inv_bind
+llpx_sn_alt_r_inv_flat
+llpx_sn_alt_r_inv_lpx_sn
+llpx_sn_alt_r_lref
+llpx_sn_alt_r_skip
+llpx_sn_alt_r_sort
+llpx_sn_bind
+llpx_sn_bind_O
+llpx_sn_bind_repl_O
+llpx_sn_bind_repl_SO
+llpx_sn_co
+llpx_sn_dec
+llpx_sn_drop_conf_O
+llpx_sn_drop_trans_O
+llpx_sn_flat
+llpx_sn_free
+llpx_sn_frees_trans
+llpx_sn_frees_trans_aux
+llpx_sn_fwd_bind_dx
+llpx_sn_fwd_bind_O_dx
+llpx_sn_fwd_bind_sn
+llpx_sn_fwd_drop_dx
+llpx_sn_fwd_drop_sn
+llpx_sn_fwd_flat_dx
+llpx_sn_fwd_flat_sn
+llpx_sn_fwd_length
+llpx_sn_fwd_lref
+llpx_sn_fwd_lref_aux
+llpx_sn_fwd_lref_dx
+llpx_sn_fwd_lref_sn
+llpx_sn_fwd_pair_sn
+llpx_sn_ge
+llpx_sn_ge_up
+llpx_sn_gref
+llpx_sn_ind_alt_r
+llpx_sn_intro_alt_r
+llpx_sn_inv_alt_r
+llpx_sn_inv_bind
+llpx_sn_inv_bind_aux
+llpx_sn_inv_bind_O
+llpx_sn_inv_flat
+llpx_sn_inv_flat_aux
+llpx_sn_inv_lift_be
+llpx_sn_inv_lift_ge
+llpx_sn_inv_lift_le
+llpx_sn_inv_lift_O
+llpx_sn_inv_lref_ge_bi
+llpx_sn_inv_lref_ge_dx
+llpx_sn_inv_lref_ge_sn
+llpx_sn_inv_S
+llpx_sn_inv_S_aux
+llpx_sn_lift_ge
+llpx_sn_lift_le
+llpx_sn_llor_dx
+llpx_sn_llor_dx_sym
+llpx_sn_llor_fwd_sn
+llpx_sn_llpx_sn_alt
+llpx_sn_lpx_sn_alt_r
+llpx_sn_lref
+llpx_sn_lrefl
+llpx_sn_lreq_repl
+llpx_sn_lreq_trans
+llpx_sn_refl
+llpx_sn_skip
+llpx_sn_sort
+llpx_sn_TC_pair_dx
+llpx_sn_Y
+LPair
+lpair_ltail
+lpr
+lpr_aaa_conf
+lpr_conf
+lpr_cpcs_conf
+lpr_cpcs_trans
+lpr_cpr_conf
+lpr_cpr_conf_dx
+lpr_cpr_conf_sn
+lpr_cprs_conf
+lpr_cprs_trans
+lpr_cpr_trans
+lpr_drop_conf
+lpr_drop_trans_O1
+lpr_fpb
+lpr_fpbq
+lpr_fwd_length
+lpr_inv_atom1
+lpr_inv_atom2
+lpr_inv_pair1
+lpr_inv_pair2
+lpr_lprs
+lpr_lpx
+lpr_pair
+lpr_refl
+lprs
+lprs_aaa_conf
+lprs_conf
+lprs_cpcs_trans
+lprs_cpr_conf_dx
+lprs_cpr_conf_sn
+lprs_cprs_conf
+lprs_cprs_conf_dx
+lprs_cprs_conf_sn
+lprs_cprs_trans
+lprs_cpr_trans
+lprs_drop_conf
+lprs_drop_trans_O1
+lprs_fpbs
+lprs_fwd_length
+lprs_ind
+lprs_ind_alt
+lprs_ind_dx
+lprs_inv_atom1
+lprs_inv_atom2
+lprs_inv_pair1
+lprs_inv_pair2
+lprs_lpxs
+lprs_pair
+lprs_pair2
+lprs_pair_refl
+lprs_refl
+lprs_strap1
+lprs_strap2
+lprs_strip
+lprs_trans
+lpx
+lpx_aaa_conf
+lpx_cpx_frees_trans
+lpx_cpxs_trans
+lpx_cpx_trans
+lpx_drop_conf
+lpx_drop_trans_O1
+lpx_fqup_trans
+lpx_fquq_trans
+lpx_fqus_trans
+lpx_fqu_trans
+lpx_frees_trans
+lpx_fwd_length
+lpx_inv_atom1
+lpx_inv_atom2
+lpx_inv_pair
+lpx_inv_pair1
+lpx_inv_pair2
+lpx_lleq_fqup_trans
+lpx_lleq_fquq_trans
+lpx_lleq_fqus_trans
+lpx_lleq_fqu_trans
+lpx_lpxs
+lpx_pair
+lpx_refl
+lpxs
+lpxs_aaa_conf
+lpxs_cpxs_trans
+lpxs_cpx_trans
+lpxs_drop_conf
+lpxs_drop_trans_O1
+lpxs_fpbg
+lpxs_fpbs
+lpxs_fpbs_trans
+lpxs_fqup_trans
+lpxs_fquq_trans
+lpxs_fqus_trans
+lpxs_fwd_length
+lpxs_ind
+lpxs_ind_alt
+lpxs_ind_dx
+lpxs_inv_atom1
+lpxs_inv_atom2
+lpxs_inv_pair1
+lpxs_inv_pair2
+lpxs_lleq_fpbs
+lpxs_lleq_fqup_trans
+lpxs_lleq_fquq_trans
+lpxs_lleq_fqus_trans
+lpxs_lleq_fqu_trans
+lpx_sn
+lpx_sn_alt
+lpx_sn_alt_atom
+lpx_sn_alt_fwd_length
+lpx_sn_alt_inv_atom1
+lpx_sn_alt_inv_atom2
+lpx_sn_alt_inv_lpx_sn
+lpx_sn_alt_inv_pair1
+lpx_sn_alt_inv_pair2
+lpx_sn_alt_pair
+lpx_sn_atom
+lpx_sn_conf
+lpx_sn_confluent
+lpx_sn_deliftable_dropable
+lpx_sn_dropable
+lpx_sn_dropable_aux
+lpx_sn_drop_conf
+lpx_sn_drop_trans
+lpx_sn_fwd_length
+lpx_sn_intro_alt
+lpx_sn_inv_alt
+lpx_sn_inv_atom1
+lpx_sn_inv_atom1_aux
+lpx_sn_inv_atom2
+lpx_sn_inv_atom2_aux
+lpx_sn_inv_pair
+lpx_sn_inv_pair1
+lpx_sn_inv_pair1_aux
+lpx_sn_inv_pair2
+lpx_sn_inv_pair2_aux
+lpx_sn_liftable_dedropable
+lpxs_nlleq_inv_step_sn
+lpx_sn_llpx_sn
+lpx_sn_lpx_sn_alt
+lpx_sn_LTC_TC_lpx_sn
+lpx_sn_pair
+lpx_sn_refl
+lpx_sn_trans
+lpx_sn_transitive
+lpxs_pair
+lpxs_pair2
+lpxs_pair_refl
+lpxs_refl
+lpxs_strap1
+lpxs_strap2
+lpxs_trans
+LRef
+lreq
+lreq_atom
+lreq_canc_dx
+lreq_canc_sn
+lreq_cpxs_trans
+lreq_cpx_trans
+lreq_drop_conf_be
+lreq_drop_trans_be
+lreq_frees_trans
+lreq_fwd_length
+lreq_inv_atom1
+lreq_inv_atom1_aux
+lreq_inv_atom2
+lreq_inv_O_Y
+lreq_inv_O_Y_aux
+lreq_inv_pair
+lreq_inv_pair1
+lreq_inv_pair1_aux
+lreq_inv_pair2
+lreq_inv_succ
+lreq_inv_succ1
+lreq_inv_succ1_aux
+lreq_inv_succ2
+lreq_inv_zero1
+lreq_inv_zero1_aux
+lreq_inv_zero2
+lreq_join
+lreq_lleq_trans
+lreq_llpx_sn_trans
+lreq_lpxs_trans_lleq
+lreq_lpxs_trans_lleq_aux
+lreq_lpx_trans_lleq
+lreq_lpx_trans_lleq_aux
+lreq_O2
+lreq_pair
+lreq_pair_lt
+lreq_pair_O_Y
+lreq_refl
+lreq_succ
+lreq_succ_lt
+lreq_sym
+lreq_trans
+lreq_zero
+lstas
+lstas_aaa_conf
+lstas_appl
+lstas_bind
+lstas_cast
+lstas_conf
+lstas_conf_le
+lstas_correct
+lstas_cpcs_lpr
+lstas_cpr
+lstas_cpr_aux
+lstas_cpr_lpr
+lstas_cpr_lpr_aux
+lstas_cprs_lpr
+lstas_cprs_lpr_aux
+lstas_cpxs
+lstas_da_conf
+lstas_fpbg
+lstas_fpbs
+lstas_inv_appl1
+lstas_inv_appl1_aux
+lstas_inv_bind1
+lstas_inv_bind1_aux
+lstas_inv_cast1
+lstas_inv_cast1_aux
+lstas_inv_da
+lstas_inv_da_ge
+lstas_inv_gref1
+lstas_inv_gref1_aux
+lstas_inv_lift1
+lstas_inv_lref1
+lstas_inv_lref1_aux
+lstas_inv_lref1_O
+lstas_inv_lref1_S
+lstas_inv_refl_pos
+lstas_inv_sort1
+lstas_inv_sort1_aux
+lstas_ldef
+lstas_lift
+lstas_llpx_sn_conf
+lstas_lstas
+lstas_mono
+lstas_scpds
+lstas_scpds_aux
+lstas_scpds_trans
+lstas_scpes_trans
+lstas_sort
+lstas_split
+lstas_split_aux
+lstas_succ
+lstas_trans
+lstas_zero
+lsuba
+lsuba_aaa_conf
+lsuba_aaa_trans
+lsuba_atom
+lsuba_beta
+lsuba_drop_O1_conf
+lsuba_drop_O1_trans
+lsuba_fwd_lsubr
+lsuba_inv_atom1
+lsuba_inv_atom1_aux
+lsuba_inv_atom2
+lsuba_inv_atom2_aux
+lsuba_inv_pair1
+lsuba_inv_pair1_aux
+lsuba_inv_pair2
+lsuba_inv_pair2_aux
+lsuba_lsubc
+lsuba_pair
+lsuba_refl
+lsuba_trans
+lsubc
+lsubc_atom
+lsubc_beta
+lsubc_drop_O1_trans
+lsubc_fwd_lsubr
+lsubc_inv_atom1
+lsubc_inv_atom1_aux
+lsubc_inv_atom2
+lsubc_inv_atom2_aux
+lsubc_inv_pair1
+lsubc_inv_pair1_aux
+lsubc_inv_pair2
+lsubc_inv_pair2_aux
+lsubc_pair
+lsubc_refl
+lsubd
+lsubd_atom
+lsubd_beta
+lsubd_da_conf
+lsubd_da_trans
+lsubd_drop_O1_conf
+lsubd_drop_O1_trans
+lsubd_fwd_lsubr
+lsubd_inv_atom1
+lsubd_inv_atom1_aux
+lsubd_inv_atom2
+lsubd_inv_atom2_aux
+lsubd_inv_pair1
+lsubd_inv_pair1_aux
+lsubd_inv_pair2
+lsubd_inv_pair2_aux
+lsubd_pair
+lsubd_refl
+lsubd_trans
+lsubr
+lsubr_atom
+lsubr_beta
+lsubr_cpcs_trans
+lsubr_cprs_trans
+lsubr_cpr_trans
+lsubr_cpxs_trans
+lsubr_cpx_trans
+lsubr_fwd_drop2_abbr
+lsubr_fwd_drop2_pair
+lsubr_fwd_length
+lsubr_inv_abbr2
+lsubr_inv_abbr2_aux
+lsubr_inv_abst1
+lsubr_inv_abst1_aux
+lsubr_inv_atom1
+lsubr_inv_atom1_aux
+lsubr_inv_pair1
+lsubr_inv_pair1_aux
+lsubr_pair
+lsubr_refl
+lsubr_trans
+lsubsv
+lsubsv_atom
+lsubsv_beta
+lsubsv_cpcs_trans
+lsubsv_cprs_trans
+lsubsv_drop_O1_conf
+lsubsv_drop_O1_trans
+lsubsv_fwd_lsuba
+lsubsv_fwd_lsubd
+lsubsv_fwd_lsubr
+lsubsv_inv_atom1
+lsubsv_inv_atom1_aux
+lsubsv_inv_atom2
+lsubsv_inv_atom2_aux
+lsubsv_inv_pair1
+lsubsv_inv_pair1_aux
+lsubsv_inv_pair2
+lsubsv_inv_pair2_aux
+lsubsv_lstas_trans
+lsubsv_pair
+lsubsv_refl
+lsubsv_scpds_trans
+lsubsv_snv_trans
+lsubsv_sta_trans
+lsuby
+lsuby_atom
+lsuby_cpysa_trans
+lsuby_cpys_trans
+lsuby_cpy_trans
+lsuby_drop_trans_be
+lsuby_fwd_length
+lsuby_inv_atom1
+lsuby_inv_atom1_aux
+lsuby_inv_pair1
+lsuby_inv_pair1_aux
+lsuby_inv_pair2
+lsuby_inv_pair2_aux
+lsuby_inv_succ1
+lsuby_inv_succ1_aux
+lsuby_inv_succ2
+lsuby_inv_succ2_aux
+lsuby_inv_zero1
+lsuby_inv_zero1_aux
+lsuby_inv_zero2
+lsuby_inv_zero2_aux
+lsuby_O2
+lsuby_pair
+lsuby_pair_lt
+lsuby_pair_O_Y
+lsuby_refl
+lsuby_succ
+lsuby_succ_lt
+lsuby_sym
+lsuby_trans
+lsuby_zero
+lsx
+lsxa
+lsxa_ind
+lsxa_intro
+lsxa_intro_aux
+lsxa_intro_lpx
+lsxa_inv_lsx
+lsxa_lleq_trans
+lsxa_lpxs_trans
+lsx_atom
+lsx_bind
+lsx_bind_lpxs_aux
+lsx_cpx_trans_lcosx
+lsx_cpx_trans_O
+lsx_flat
+lsx_flat_lpxs
+lsx_fwd_bind_dx
+lsx_fwd_bind_sn
+lsx_fwd_flat_dx
+lsx_fwd_flat_sn
+lsx_fwd_lref_be
+lsx_fwd_pair_sn
+lsx_ge
+lsx_ge_up
+lsx_gref
+lsx_ind
+lsx_ind_alt
+lsx_intro
+lsx_intro_alt
+lsx_inv_bind
+lsx_inv_flat
+lsx_inv_lift_be
+lsx_inv_lift_ge
+lsx_inv_lift_le
+lsx_lift_ge
+lsx_lift_le
+lsx_lleq_trans
+lsx_lpxs_trans
+lsx_lpx_trans
+lsx_lref_be
+lsx_lref_be_lpxs
+lsx_lref_free
+lsx_lref_skip
+lsx_lreq_conf
+lsx_lsxa
+lsx_sort
+ltail_length
+lw
+lw_pair
+minuss
+minuss_ge
+minuss_inv_cons1
+minuss_inv_cons1_aux
+minuss_inv_cons1_ge
+minuss_inv_cons1_lt
+minuss_inv_nil1
+minuss_inv_nil1_aux
+minuss_lt
+minuss_nil
+mk_gcp
+mk_gcr
+mk_sd
+mk_sh
+nexts_dec
+nexts_inj
+nexts_le
+nexts_lt
+nf
+nlift_bind_dx
+nlift_bind_sn
+nlift_flat_dx
+nlift_flat_sn
+nlift_inv_bind
+nlift_inv_flat
+nlift_inv_lref_be_SO
+nlift_lref_be_SO
+nlleq_inv_bind
+nlleq_inv_bind_O
+nlleq_inv_flat
+nlleq_lleq_div
+nllpx_sn_inv_bind
+nllpx_sn_inv_bind_O
+nllpx_sn_inv_flat
+Omega1
+Omega2
+pluss
+pluss_inv_cons2
+pluss_inv_nil2
+rfw
+rfw_lpair_dx
+rfw_lpair_sn
+rfw_shift
+rfw_tpair_dx
+rfw_tpair_sn
+ri2
+S1
+S2
+S3
+S4
+S5
+S6
+S7
+scpds
+scpds_aaa_conf
+scpds_conf_eq
+scpds_cpr_lpr_aux
+scpds_cprs_trans
+scpds_div
+scpds_fwd_cprs
+scpds_fwd_cpxs
+scpds_inv_abbr_abst
+scpds_inv_abst1
+scpds_inv_lift1
+scpds_inv_lstas_eq
+scpds_lift
+scpds_strap1
+scpds_strap2
+scpes
+scpes_aaa_mono
+scpes_canc_dx
+scpes_canc_sn
+scpes_cpr_lpr_aux
+scpes_inv_abst2
+scpes_inv_lstas_eq
+scpes_le_aux
+scpes_refl
+scpes_sym
+scpes_trans
+sd
+sd_d
+sd_d_correct
+sd_d_SS
+sd_O
+sd_SO
+sh
+sh_N
+shnv
+shnv_cast
+shnv_inv_cast
+shnv_inv_cast_aux
+shnv_inv_snv
+simple
+simple_atom
+simple_flat
+simple_inv_bind
+simple_inv_bind_aux
+simple_inv_pair
+simple_tsts_repl_dx
+simple_tsts_repl_sn
+snv
+snv_appl
+snv_bind
+snv_cast
+snv_cast_scpes
+snv_cpr_lpr
+snv_cpr_lpr_aux
+snv_cprs_lpr
+snv_cprs_lpr_aux
+snv_extended
+snv_fqu_conf
+snv_fqup_conf
+snv_fquq_conf
+snv_fqus_conf
+snv_fwd_aaa
+snv_fwd_da
+snv_fwd_fsb
+snv_fwd_lstas
+snv_inv_appl
+snv_inv_appl_aux
+snv_inv_bind
+snv_inv_bind_aux
+snv_inv_cast
+snv_inv_cast_aux
+snv_inv_gref
+snv_inv_gref_aux
+snv_inv_lift
+snv_inv_lref
+snv_inv_lref_aux
+snv_lift
+snv_lref
+snv_lstas
+snv_lstas_aux
+snv_preserve
+snv_restricted
+snv_shnv_cast
+snv_sort
+Sort
+sta_cprs_scpds
+sta_cpx
+sta_cpx_aux
+sta_fpb
+sta_fpbg
+sta_fpbq
+sta_fpbs
+sta_ldec
+TAtom
+TC_lpx_sn_fwd_length
+TC_lpx_sn_ind
+TC_lpx_sn_inv_atom1
+TC_lpx_sn_inv_atom2
+TC_lpx_sn_inv_lpx_sn_LTC
+TC_lpx_sn_inv_pair1
+TC_lpx_sn_inv_pair1_aux
+TC_lpx_sn_inv_pair2
+TC_lpx_sn_pair
+TC_lpx_sn_pair_refl
+term
+tir_atom
+tix_lref
+TPair
+tpr_cpr
+tprs_cprs
+trr_inv_atom
+trx_inv_atom
+tsts
+tsts_atom
+tsts_canc_dx
+tsts_canc_sn
+tsts_dec
+tsts_inv_atom1
+tsts_inv_atom1_aux
+tsts_inv_atom2
+tsts_inv_atom2_aux
+tsts_inv_bind_applv_simple
+tsts_inv_pair1
+tsts_inv_pair1_aux
+tsts_inv_pair2
+tsts_inv_pair2_aux
+tsts_pair
+tsts_refl
+tsts_sym
+tsts_trans
+tw
+tw_pos
+unfold
+unfold_bind
+unfold_flat
+unfold_lref
+unfold_sort
]
qed-.
-lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
+lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
/2 width=4 by lsuba_inv_atom2_aux/ qed-.
fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
--- /dev/null
+NAMING CONVENTIONS FOR METAVARIABLES
+
+A,B : arity
+C : candidate of reducibility
+D,E : RTM environment
+F,G : global environment
+H : reserved: transient premise
+IH : reserved: inductive premise
+I,J : item
+K,L : local environment
+M,N : reserved: future use
+O :
+P : relocation environment
+Q : elimination predicate
+R : generic predicate/relation
+S : RTM stack
+T,U,V,W: term
+X,Y,Z : reserved: transient objet denoted by a capital letter
+
+a : applicability condition (true = restricted, false = general)
+b : local dropping kind parameter (true = restricted, false = general)
+c : rt-reduction count parameter
+d : term degree
+e : reserved: future use (\lambda\delta 3)
+f,g : local reference transforming map
+h : sort hierarchy parameter
+i,j : local reference depth (de Bruijn's)
+k,l : global reference level
+m,n : iterations
+o : sort degree parameter (origin)
+p,q : binder polarity
+r :
+s : sort index
+t,u :
+v,w : local reference position level (de Bruijn's) (RTM)
+x,y,z : reserved: transient objet denoted by a small letter
+
+NAMING CONVENTIONS FOR CONSTRUCTORS
+
+0: atomic
+2: binary
+
+A: application to vector
+E: empty list
+F: boolean false
+T: boolean true
+
+a: application
+b: generic binder with one argument
+d: abbreviation
+f: generic flat with one argument
+i: generic binder for local environments
+l: typed abstraction
+n: native type annotation
+u: generic binder with zero argument
+x: exclusion
+
+NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
+
+- prefix and first letter
+
+b: bi contex-sensitive for local environments
+c: contex-sensitive for terms
+f: context-freee for closures
+l: sn contex-sensitive for local environments
+r: dx contex-sensitive for local environments
+s: stratified (prefix)
+t: context-free for terms
+
+- second letter
+
+e: reserved for generic entrywise extension
+i: irreducible form
+n: normal form
+p: reflexive parallel transformation
+q: sequential transformation
+r: reducible form
+s: strongly normalizing form
+
+- third letter
+
+b: (q)rst-reduction
+c: conversion
+d: decomposed rt-reduction
+e: decomposed rt-conversion
+g: counted rt-transition (generic)
+m: semi-counted rt-transition (mixed)
+q: restricted reduction
+r: reduction
+s: substitution
+u: supclosure
+w: reserved for generic pointwise extension
+x: uncounted rt-transition (extended)
+y: rt-substitution
+
+- forth letter (if present)
+
+c: proper single step (general) (successor)
+e: reflexive transitive closure to normal form (evaluation)
+g: proper multiple step (general) (greater)
+p: non-reflexive transitive closure (plus)
+q: reflexive closure (question)
+r: proper multiple step (restricted) (restricted)
+s: reflexive transitive closure (star)
+u: proper single step (restricted) (unit)
--- /dev/null
+aaa
+aaa_aaa_inv_appl
+aaa_aaa_inv_cast
+aaa_abbr
+aaa_abst
+aaa_appl
+aaa_cast
+aaa_dec
+aaa_feqx_conf
+aaa_fqu_conf
+aaa_fqup_conf
+aaa_fquq_conf
+aaa_fqus_conf
+aaa_inv_abbr
+aaa_inv_abbr_aux
+aaa_inv_abst
+aaa_inv_abst_aux
+aaa_inv_appl
+aaa_inv_appl_aux
+aaa_inv_cast
+aaa_inv_cast_aux
+aaa_inv_gref
+aaa_inv_gref_aux
+aaa_inv_lifts
+aaa_inv_lref
+aaa_inv_lref_aux
+aaa_inv_lref_drops
+aaa_inv_sort
+aaa_inv_sort_aux
+aaa_inv_zero
+aaa_inv_zero_aux
+aaa_lifts
+aaa_lref
+aaa_lref_drops
+aaa_mono
+aaa_pair_inv_lref
+aaa_sort
+aaa_teqx_conf_reqx
+aaa_zero
+aarity
+AAtom
+Abbr
+Abst
+abst_dec
+ac
+ac_eq
+ac_eq_props
+ac_le
+acle
+acle_eq_le
+acle_eq_monotonic_le
+acle_le_eq
+acle_le_monotonic_le
+acle_omega
+acle_one
+ac_le_props
+acle_refl
+acle_trans
+ac_props
+acr
+acr_aaa
+acr_aaa_csubc_lifts
+acr_abst
+acr_gcr
+acr_lifts
+ac_top
+ac_top_props
+APair
+append
+append_assoc
+append_atom
+append_atom_sn
+append_bind
+append_inj_dx
+append_inj_length_dx
+append_inj_length_sn
+append_inj_sn
+append_inv_atom3_sn
+append_inv_bind3_sn
+append_inv_pair_dx
+append_inv_refl_dx
+append_length
+append_shift
+Appl
+applv
+applv_cons
+applv_nil
+applv_simple
+apply_top
+bind
+bind1
+bind2
+Bind2
+BPair
+BUnit
+bw
+bw_pos
+candidate
+Cast
+cdeq
+cdeq_ext
+ceq
+ceq_ext
+ceq_ext_inv_eq
+ceq_ext_refl
+ceq_ext_trans
+ceq_inv_lift_sn
+ceq_lift_sn
+cext2
+cext2_co
+cext2_d_liftable2_sn
+cext2_sym
+cfull
+cfull_dec
+cfull_lift_sn
+cfun
+co_dedropable_sn
+co_dedropable_sn_CTC
+co_dedropable_sn_ltc
+co_dropable_dx
+co_dropable_dx_CTC
+co_dropable_dx_ltc
+co_dropable_sn
+co_dropable_sn_CTC
+co_dropable_sn_ltc
+CP0
+CP1
+CP2
+CP3
+d1_liftable_liftable_all
+d2_deliftable_sn_CTC
+d2_deliftable_sn_ltc
+d2_liftable_sn_CTC
+d2_liftable_sn_ltc
+d_appendable_sn
+d_deliftable1
+d_deliftable1_isuni
+d_deliftable2_bi
+d_deliftable2_sn
+d_deliftable2_sn_bi
+dedropable_sn
+dedropable_sn_CTC
+deg_inv_prec
+deg_inv_pred
+deg_iter
+deg_next_SO
+deg_O
+deg_SO
+deg_SO_gt
+deg_SO_inv_succ
+deg_SO_inv_succ_aux
+deg_SO_refl
+deg_SO_succ
+deg_SO_zero
+deliftable2_bi
+deliftable2_dx
+deliftable2_sn
+deliftable2_sn_bi
+deliftable2_sn_dx
+destruct_apair_apair_aux
+destruct_lbind_lbind_aux
+destruct_sort_sort_aux
+destruct_tatom_tatom_aux
+destruct_tpair_tpair_aux
+discr_apair_xy_x
+discr_apair_xy_y
+discr_lbind_x_xy
+discr_lbind_xy_x
+discr_tpair_xy_x
+discr_tpair_xy_y
+d_liftable1
+d_liftable1_all
+d_liftable1_isuni
+d_liftable2_bi
+d_liftable2_sn
+d_liftable2_sn_bi
+dropable_dx
+dropable_dx_CTC
+dropable_sn
+dropable_sn_CTC
+drops
+drops_after_fwd_drop2
+drops_atom
+drops_atom2_sex_conf
+drops_atom_F
+drops_bind2_fwd_rfw
+drops_conf
+drops_conf_div
+drops_conf_div_bind_isuni
+drops_conf_div_fcla
+drops_conf_div_isuni
+drops_conf_skip1
+drops_drop
+drops_eq_repl_back
+drops_eq_repl_fwd
+drops_F
+drops_fcla_fwd
+drops_fcla_fwd_le2
+drops_fcla_fwd_lt2
+drops_fcla_fwd_lt4
+drops_F_uni
+drops_fwd_drop2
+drops_fwd_drop2_aux
+drops_fwd_fcla
+drops_fwd_fcla_le2
+drops_fwd_fcla_lt2
+drops_fwd_isfin
+drops_fwd_isid
+drops_fwd_length_eq1
+drops_fwd_length_eq2
+drops_fwd_length_le4
+drops_fwd_lw
+drops_fwd_lw_lt
+drops_gen
+drops_inv_atom1
+drops_inv_atom1_aux
+drops_inv_atom2
+drops_inv_bind1_isuni
+drops_inv_bind2_isuni
+drops_inv_bind2_isuni_next
+drops_inv_drop1
+drops_inv_drop1_aux
+drops_inv_F
+drops_inv_gen
+drops_inv_isuni
+drops_inv_length_eq
+drops_inv_skip1
+drops_inv_skip1_aux
+drops_inv_skip2
+drops_inv_skip2_aux
+drops_inv_succ
+drops_inv_TF
+drops_inv_TF_aux
+drops_inv_uni
+drops_inv_x_bind_xy
+drops_isuni_ex
+drops_isuni_fwd_drop2
+drops_ldec_dec
+drops_lsubc_trans
+drops_mono
+drops_refl
+drops_seq_trans_next
+drops_sex_trans_next
+drops_sex_trans_push
+drops_skip
+drops_split_div
+drops_split_trans
+drops_split_trans_bind2
+drops_TF
+drops_tls_at
+drops_trans
+drops_trans_skip2
+eq_aarity_dec
+eq_bind1_dec
+eq_bind2_dec
+eq_bind_dec
+eq_false_inv_tpair_dx
+eq_false_inv_tpair_sn
+eq_flat2_dec
+eq_genv_dec
+eq_item0_dec
+eq_item2_dec
+eq_lenv_dec
+eq_term_dec
+ext2
+ext2_dec
+ext2_inv_pair
+ext2_inv_pair_dx
+ext2_inv_pair_dx_aux
+ext2_inv_pair_sn
+ext2_inv_pair_sn_aux
+ext2_inv_tc
+ext2_inv_unit
+ext2_inv_unit_dx
+ext2_inv_unit_dx_aux
+ext2_inv_unit_sn
+ext2_inv_unit_sn_aux
+ext2_pair
+ext2_refl
+ext2_sym
+ext2_tc
+ext2_tc_inj
+ext2_tc_pair
+ext2_tc_step
+ext2_trans
+ext2_unit
+f_dedropable_sn
+f_dropable_dx
+f_dropable_sn
+feqx
+feqx_canc_dx
+feqx_canc_sn
+feqx_fqus_trans
+feqx_intro_dx
+feqx_intro_sn
+feqx_inv_gen_dx
+feqx_inv_gen_sn
+feqx_refl
+feqx_sym
+feqx_tneqx_repl_dx
+feqx_trans
+flat2
+Flat2
+fold
+fold_atom
+fold_pair
+fold_unit
+fqu
+fqu_bind_dx
+fqu_clear
+fqu_drop
+fqu_flat_dx
+fqu_fqup
+fqu_fquq
+fqu_fwd_fw
+fqu_fwd_length_lref1
+fqu_fwd_length_lref1_aux
+fqu_gref
+fqu_inv_atom1
+fqu_inv_bind1
+fqu_inv_bind1_aux
+fqu_inv_bind1_true
+fqu_inv_flat1
+fqu_inv_flat1_aux
+fqu_inv_gref1
+fqu_inv_gref1_aux
+fqu_inv_gref1_bind
+fqu_inv_lref1
+fqu_inv_lref1_aux
+fqu_inv_lref1_bind
+fqu_inv_sort1
+fqu_inv_sort1_aux
+fqu_inv_sort1_bind
+fqu_inv_teqx
+fqu_inv_teqx_aux
+fqu_inv_zero1_pair
+fqu_lref_O
+fqu_lref_S
+fqup
+fqu_pair_sn
+fqup_bind_dx
+fqup_bind_dx_flat_dx
+fqup_clear
+fqup_drops_strap1
+fqup_drops_succ
+fqup_flat_dx
+fqup_flat_dx_bind_dx
+fqup_flat_dx_pair_sn
+fqup_fqus
+fqup_fqus_trans
+fqup_fwd_fw
+fqup_ind
+fqup_ind_dx
+fqup_inv_step_sn
+fqup_lref
+fqup_pair_sn
+fqup_strap1
+fqup_strap2
+fqup_trans
+fqup_wf_ind
+fqup_wf_ind_eq
+fqup_zeta
+fquq
+fquq_fqus
+fquq_fwd_fw
+fquq_fwd_length_lref1
+fquq_refl
+fqus
+fqus_drops
+fqus_fqup_trans
+fqus_fwd_fw
+fqus_ind
+fqus_ind_dx
+fqus_inv_atom1
+fqus_inv_bind1
+fqus_inv_bind1_true
+fqus_inv_flat1
+fqus_inv_fqup
+fqus_inv_fqu_sn
+fqus_inv_gref1
+fqus_inv_gref1_bind
+fqus_inv_lref1
+fqus_inv_lref1_bind
+fqus_inv_refl_atom3
+fqus_inv_sort1
+fqus_inv_sort1_bind
+fqus_inv_zero1_pair
+fqu_sort
+fqus_refl
+fqus_strap1
+fqus_strap1_fqu
+fqus_strap2
+fqus_strap2_fqu
+fqus_trans
+fqu_teqx_conf
+fqu_wf_ind
+frees
+frees_append_void
+frees_atom
+frees_atom_drops
+frees_bind
+frees_bind_void
+frees_eq_repl_back
+frees_eq_repl_fwd
+frees_flat
+frees_fwd_coafter
+frees_fwd_isfin
+frees_gref
+frees_ind_void
+frees_inv_append_void
+frees_inv_append_void_aux
+frees_inv_atom
+frees_inv_atom_aux
+frees_inv_bind
+frees_inv_bind_aux
+frees_inv_bind_void
+frees_inv_drops_next
+frees_inv_flat
+frees_inv_flat_aux
+frees_inv_gref
+frees_inv_gref_aux
+frees_inv_lifts
+frees_inv_lifts_ex
+frees_inv_lifts_SO
+frees_inv_lref
+frees_inv_lref_aux
+frees_inv_lref_drops
+frees_inv_pair
+frees_inv_pair_aux
+frees_inv_sort
+frees_inv_sort_aux
+frees_inv_unit
+frees_inv_unit_aux
+frees_lifts
+frees_lifts_SO
+frees_lref
+frees_lref_push
+frees_lref_pushs
+frees_mono
+frees_pair
+frees_pair_drops
+frees_req_conf
+frees_reqx_conf
+frees_sex_conf
+frees_sort
+frees_teqx_conf
+frees_teqx_conf_reqx
+frees_total
+frees_unit
+frees_unit_drops
+fsge_rex_trans
+fsle
+fsle_bind
+fsle_bind_dx_dx
+fsle_bind_dx_sn
+fsle_bind_eq
+fsle_bind_sn_ge
+fsle_flat
+fsle_flat_dx_dx
+fsle_flat_dx_sn
+fsle_flat_sn
+fsle_frees_trans
+fsle_frees_trans_eq
+fsle_fwd_pair_sn
+fsle_gref
+fsle_gref_bi
+fsle_inv_frees_eq
+fsle_inv_lifts_sn
+fsle_lifts_dx
+fsle_lifts_sn
+fsle_lifts_SO
+fsle_lifts_SO_sn
+fsle_pair_bi
+fsle_refl
+fsle_shift
+fsle_sort
+fsle_sort_bi
+fsle_trans_dx
+fsle_trans_rc
+fsle_trans_sn
+fsle_unit_bi
+f_transitive_next
+fw
+fw_clear
+fw_lpair_sn
+fw_shift
+fw_tpair_dx
+fw_tpair_sn
+GAtom
+gcp
+gcp2_all
+gcr
+gcr_aaa
+genv
+glength
+GPair
+GRef
+gw
+gw_pair
+is_apear_dec
+is_lifts_dec
+item0
+item2
+LAtom
+LBind
+length
+length_atom
+length_bind
+length_inv_succ_dx
+length_inv_succ_dx_ltail
+length_inv_succ_sn
+length_inv_succ_sn_ltail
+length_inv_zero_dx
+length_inv_zero_sn
+lenv
+lenv_case_tail
+lenv_ind_tail
+lex
+lex_atom
+lex_bind
+lex_bind_refl_dx
+lex_co
+lex_conf
+lex_confluent
+lex_CTC
+lex_CTC_ind_dx
+lex_CTC_ind_sn
+lex_CTC_inj
+lex_CTC_step_dx
+lex_CTC_step_sn
+lex_dropable_dx
+lex_dropable_sn
+lex_drops_conf_pair
+lex_drops_trans_pair
+lex_fwd_length
+lex_ind
+lex_inv_atom_dx
+lex_inv_atom_sn
+lex_inv_bind_dx
+lex_inv_bind_sn
+lex_inv_CTC
+lex_inv_pair
+lex_inv_pair_dx
+lex_inv_pair_sn
+lex_inv_unit_dx
+lex_inv_unit_sn
+lex_liftable_dedropable_sn
+lex_pair
+lex_refl
+lex_trans
+lex_transitive
+lex_unit
+liftable2_bi
+liftable2_dx
+liftable2_sn
+liftable2_sn_bi
+liftable2_sn_dx
+lifts
+lifts_applv
+liftsb
+liftsb_conf
+liftsb_div3
+liftsb_eq_repl_back
+liftsb_fwd_bw
+liftsb_fwd_isid
+lifts_bind
+liftsb_inj
+liftsb_inv_pair_dx
+liftsb_inv_pair_sn
+liftsb_inv_unit_dx
+liftsb_inv_unit_sn
+liftsb_mono
+liftsb_refl
+liftsb_split_trans
+liftsb_total
+liftsb_trans
+lifts_conf
+lifts_div3
+lifts_div4
+lifts_div4_one
+lifts_eq_repl_back
+lifts_eq_repl_fwd
+lifts_flat
+lifts_fwd_isid
+lifts_fwd_pair1
+lifts_fwd_pair2
+lifts_fwd_tw
+lifts_gref
+lifts_inj
+lifts_inv_applv1
+lifts_inv_applv2
+lifts_inv_atom1
+lifts_inv_atom2
+lifts_inv_bind1
+lifts_inv_bind1_aux
+lifts_inv_bind2
+lifts_inv_bind2_aux
+lifts_inv_flat1
+lifts_inv_flat1_aux
+lifts_inv_flat2
+lifts_inv_flat2_aux
+lifts_inv_gref1
+lifts_inv_gref1_aux
+lifts_inv_gref2
+lifts_inv_gref2_aux
+lifts_inv_lref1
+lifts_inv_lref1_aux
+lifts_inv_lref1_uni
+lifts_inv_lref2
+lifts_inv_lref2_aux
+lifts_inv_lref2_uni
+lifts_inv_lref2_uni_ge
+lifts_inv_lref2_uni_lt
+lifts_inv_pair_xy_x
+lifts_inv_pair_xy_y
+lifts_inv_push_succ_sn
+lifts_inv_push_zero_sn
+lifts_inv_sort1
+lifts_inv_sort1_aux
+lifts_inv_sort2
+lifts_inv_sort2_aux
+lifts_lref
+lifts_lref_ge
+lifts_lref_ge_minus
+lifts_lref_lt
+lifts_lref_uni
+lifts_mono
+lifts_push_lref
+lifts_push_zero
+lifts_refl
+lifts_simple_dx
+lifts_simple_sn
+lifts_sort
+lifts_split_div
+lifts_split_trans
+lifts_total
+lifts_trans
+lifts_trans4_one
+lifts_trans_uni
+lifts_uni
+liftsv
+liftsv_cons
+liftsv_inj
+liftsv_inv_cons1
+liftsv_inv_cons1_aux
+liftsv_inv_cons2
+liftsv_inv_cons2_aux
+liftsv_inv_nil1
+liftsv_inv_nil1_aux
+liftsv_inv_nil2
+liftsv_inv_nil2_aux
+liftsv_mono
+liftsv_nil
+liftsv_split_trans
+liftsv_total
+liftsv_trans
+LRef
+lsuba
+lsuba_aaa_conf
+lsuba_aaa_trans
+lsuba_atom
+lsuba_beta
+lsuba_bind
+lsuba_drops_conf_isuni
+lsuba_drops_trans_isuni
+lsuba_fwd_lsubr
+lsuba_inv_atom1
+lsuba_inv_atom1_aux
+lsuba_inv_atom2
+lsuba_inv_atom2_aux
+lsuba_inv_bind1
+lsuba_inv_bind1_aux
+lsuba_inv_bind2
+lsuba_inv_bind2_aux
+lsuba_lsubc
+lsuba_refl
+lsuba_trans
+lsubc
+lsubc_atom
+lsubc_beta
+lsubc_bind
+lsubc_drops_trans_isuni
+lsubc_fwd_lsubr
+lsubc_inv_atom1
+lsubc_inv_atom1_aux
+lsubc_inv_atom2
+lsubc_inv_atom2_aux
+lsubc_inv_bind1
+lsubc_inv_bind1_aux
+lsubc_inv_bind2
+lsubc_inv_bind2_aux
+lsubc_refl
+lsubf
+lsubf_atom
+lsubf_beta
+lsubf_beta_tl_dx
+lsubf_bind
+lsubf_bind_tl_dx
+lsubf_eq_repl_back1
+lsubf_eq_repl_back2
+lsubf_eq_repl_fwd1
+lsubf_eq_repl_fwd2
+lsubf_frees_trans
+lsubf_fwd_bind_tl
+lsubf_fwd_isid_dx
+lsubf_fwd_isid_sn
+lsubf_fwd_lsubr_isdiv
+lsubf_fwd_sle
+lsubf_inv_atom
+lsubf_inv_atom1
+lsubf_inv_atom1_aux
+lsubf_inv_atom2
+lsubf_inv_atom2_aux
+lsubf_inv_beta_sn
+lsubf_inv_bind_sn
+lsubf_inv_pair1
+lsubf_inv_pair1_aux
+lsubf_inv_pair2
+lsubf_inv_pair2_aux
+lsubf_inv_push1
+lsubf_inv_push1_aux
+lsubf_inv_push2
+lsubf_inv_push2_aux
+lsubf_inv_push_sn
+lsubf_inv_refl
+lsubf_inv_sor_dx
+lsubf_inv_unit1
+lsubf_inv_unit1_aux
+lsubf_inv_unit2
+lsubf_inv_unit2_aux
+lsubf_inv_unit_sn
+lsubf_push
+lsubf_refl
+lsubf_refl_eq
+lsubf_sor
+lsubf_unit
+lsubr
+lsubr_atom
+lsubr_beta
+lsubr_bind
+lsubr_fwd_bind1
+lsubr_fwd_bind2
+lsubr_fwd_drops2_abbr
+lsubr_fwd_drops2_bind
+lsubr_fwd_length
+lsubr_inv_abbr2
+lsubr_inv_abst1
+lsubr_inv_abst2
+lsubr_inv_atom1
+lsubr_inv_atom1_aux
+lsubr_inv_atom2
+lsubr_inv_atom2_aux
+lsubr_inv_bind1
+lsubr_inv_bind1_aux
+lsubr_inv_bind2
+lsubr_inv_bind2_aux
+lsubr_inv_pair2
+lsubr_inv_unit1
+lsubr_inv_unit2
+lsubr_lsubf
+lsubr_lsubf_isid
+lsubr_refl
+lsubr_trans
+lsubr_unit
+ltail_length
+lveq
+lveq_atom
+lveq_bind
+lveq_fwd_abst_bind_length_le
+lveq_fwd_bind_abst_length_le
+lveq_fwd_gen
+lveq_fwd_length
+lveq_fwd_length_eq
+lveq_fwd_length_le_dx
+lveq_fwd_length_le_sn
+lveq_fwd_length_minus
+lveq_fwd_length_plus
+lveq_fwd_pair_dx
+lveq_fwd_pair_sn
+lveq_inj
+lveq_inj_length
+lveq_inj_void_dx_le
+lveq_inj_void_sn_ge
+lveq_inv_atom_atom
+lveq_inv_atom_bind
+lveq_inv_bind
+lveq_inv_bind_atom
+lveq_inv_bind_O
+lveq_inv_pair_pair
+lveq_inv_succ
+lveq_inv_succ_aux
+lveq_inv_succ_dx
+lveq_inv_succ_sn
+lveq_inv_succ_sn_aux
+lveq_inv_void_dx_length
+lveq_inv_void_sn_length
+lveq_inv_void_succ_dx
+lveq_inv_void_succ_sn
+lveq_inv_zero
+lveq_inv_zero_aux
+lveq_length_eq
+lveq_length_fwd_dx
+lveq_length_fwd_sn
+lveq_refl
+lveq_sym
+lveq_void_dx
+lveq_void_sn
+lw
+lw_bind
+mk_ac
+mk_ac_props
+mk_gcp
+mk_gcr
+mk_sd
+mk_sd_props
+mk_sh
+mk_sh_acyclic
+mk_sh_decidable
+mk_sh_lt
+nexts_le
+nexts_lt
+nf
+R_confluent2_rex
+req
+req_feqx_trans
+req_fsle_comp
+req_fwd_rex
+req_inv_bind
+req_inv_flat
+req_inv_lifts_bi
+req_inv_lref_bind_dx
+req_inv_lref_bind_sn
+req_inv_zero_pair_dx
+req_inv_zero_pair_sn
+req_refl
+req_reqx
+req_reqx_trans
+req_rex_trans
+req_transitive
+reqx
+reqx_atom
+reqx_bind
+reqx_bind_repl_dx
+reqx_bind_void
+reqx_canc_dx
+reqx_canc_sn
+reqx_dec
+reqx_flat
+reqx_fqup_trans
+reqx_fquq_trans
+reqx_fqus_trans
+reqx_fqu_trans
+reqx_fsge_comp
+reqx_fwd_bind_dx
+reqx_fwd_bind_dx_void
+reqx_fwd_dx
+reqx_fwd_flat_dx
+reqx_fwd_length
+reqx_fwd_pair_sn
+reqx_fwd_zero_pair
+reqx_gref
+reqx_gref_length
+reqx_inv_atom_dx
+reqx_inv_atom_sn
+reqx_inv_bind
+reqx_inv_bind_void
+reqx_inv_flat
+reqx_inv_lifts_bi
+reqx_inv_lifts_dx
+reqx_inv_lifts_sn
+reqx_inv_lref
+reqx_inv_lref_bind_dx
+reqx_inv_lref_bind_sn
+reqx_inv_lref_pair_bi
+reqx_inv_lref_pair_dx
+reqx_inv_lref_pair_sn
+reqx_inv_zero
+reqx_inv_zero_pair_dx
+reqx_inv_zero_pair_sn
+reqx_lifts_bi
+reqx_lifts_sn
+reqx_lref
+reqx_pair
+reqx_pair_refl
+reqx_refl
+reqx_repl
+reqx_rneqx_trans
+reqx_sort
+reqx_sort_length
+reqx_sym
+reqx_trans
+reqx_unit
+reqx_unit_length
+rex
+rex_atom
+rex_bind
+rex_bind_dx_split
+rex_bind_dx_split_void
+rex_bind_repl_dx
+rex_bind_void
+rex_co
+rex_conf
+rex_confluent
+rex_dec
+rex_dropable_dx
+rex_dropable_sn
+rex_flat
+rex_flat_dx_split
+rex_fsge_compatible
+rex_fsle_compatible
+rex_fwd_bind_dx
+rex_fwd_bind_dx_void
+rex_fwd_dx
+rex_fwd_flat_dx
+rex_fwd_length
+rex_fwd_pair_sn
+rex_fwd_zero_pair
+rex_gref
+rex_gref_length
+rex_inv_atom_dx
+rex_inv_atom_sn
+rex_inv_bind
+rex_inv_bind_void
+rex_inv_flat
+rex_inv_frees
+rex_inv_gref
+rex_inv_gref_bind_dx
+rex_inv_gref_bind_sn
+rex_inv_lex_req
+rex_inv_lifts_bi
+rex_inv_lref
+rex_inv_lref_bind_dx
+rex_inv_lref_bind_sn
+rex_inv_lref_pair_bi
+rex_inv_lref_pair_dx
+rex_inv_lref_pair_sn
+rex_inv_lref_unit_dx
+rex_inv_lref_unit_sn
+rex_inv_sort
+rex_inv_sort_bind_dx
+rex_inv_sort_bind_sn
+rex_inv_zero
+rex_inv_zero_length
+rex_inv_zero_pair_dx
+rex_inv_zero_pair_sn
+rex_inv_zero_unit_dx
+rex_inv_zero_unit_sn
+rex_isid
+rex_lex
+rex_liftable_dedropable_sn
+rex_lifts_bi
+rex_lref
+rex_pair
+rex_pair_refl
+rex_pair_sn_split
+rex_refl
+rexs
+rexs_atom
+rexs_co
+rexs_fwd_bind_dx
+rexs_fwd_bind_dx_void
+rexs_fwd_flat_dx
+rexs_fwd_length
+rexs_fwd_pair_sn
+rexs_gref
+rexs_ind_dx
+rexs_ind_sn
+rexs_inv_atom_dx
+rexs_inv_atom_sn
+rexs_inv_bind
+rexs_inv_bind_void
+rexs_inv_flat
+rexs_inv_gref
+rexs_inv_gref_bind_dx
+rexs_inv_gref_bind_sn
+rexs_inv_lex_req
+rexs_inv_sort
+rexs_inv_sort_bind_dx
+rexs_inv_sort_bind_sn
+rexs_lex
+rexs_lex_req
+rexs_lref
+rex_sort
+rex_sort_length
+rexs_pair
+rexs_pair_refl
+rexs_refl
+rexs_sort
+rexs_step_dx
+rexs_step_sn
+rexs_sym
+rexs_tc
+rexs_trans
+rexs_unit
+rex_sym
+rex_trans_fsle
+rex_transitive
+rex_trans_next
+rex_unit
+rex_unit_length
+rex_unit_sn
+R_fsge_compatible
+rfw
+rfw_clear
+rfw_lpair_dx
+rfw_lpair_sn
+rfw_shift
+rfw_tpair_dx
+rfw_tpair_sn
+rneqx_inv_bind
+rneqx_inv_bind_void
+rneqx_inv_flat
+rneqx_reqx_canc_dx
+rneqx_reqx_div
+rnex_inv_bind
+rnex_inv_bind_void
+rnex_inv_flat
+R_pw_confluent2_sex
+S1
+S2
+S3
+S5
+S6
+S7
+sd
+sd_d
+sd_d_correct
+sd_d_props
+sd_d_SS
+sd_O
+sd_O_props
+sd_props
+sd_SO
+sd_SO_props
+seq
+seq_canc_dx
+seq_canc_sn
+seq_co_dedropable_sn
+seq_co_dropable_dx
+seq_co_dropable_sn
+seq_drops_conf_next
+seq_drops_trans_next
+seq_eq_repl_back
+seq_eq_repl_fwd
+seq_fwd_length
+seq_inv_atom1
+seq_inv_atom2
+seq_inv_next
+seq_inv_next1
+seq_inv_next2
+seq_inv_push
+seq_inv_push1
+seq_inv_push2
+seq_inv_tl
+seq_join
+seq_meet
+seq_refl
+seq_sym
+seq_trans
+sex
+sex_atom
+sex_canc_dx
+sex_canc_sn
+sex_co
+sex_co_dropable_dx
+sex_co_dropable_sn
+sex_co_isid
+sex_conf
+sex_dec
+sex_dropable_dx_aux
+sex_drops_conf_next
+sex_drops_conf_push
+sex_drops_trans_next
+sex_drops_trans_push
+sex_eq_repl_back
+sex_eq_repl_fwd
+sex_fwd_bind
+sex_fwd_length
+sex_inv_atom1
+sex_inv_atom1_aux
+sex_inv_atom2
+sex_inv_atom2_aux
+sex_inv_next
+sex_inv_next1
+sex_inv_next1_aux
+sex_inv_next2
+sex_inv_next2_aux
+sex_inv_push
+sex_inv_push1
+sex_inv_push1_aux
+sex_inv_push2
+sex_inv_push2_aux
+sex_inv_tc_dx
+sex_inv_tc_sn
+sex_inv_tl
+sex_join
+sex_length_cfull
+sex_length_isid
+sex_liftable_co_dedropable_bi
+sex_liftable_co_dedropable_sn
+sex_meet
+sex_next
+sex_pair_repl
+sex_push
+sex_refl
+sex_sdj
+sex_sdj_split
+sex_sle_split
+sex_sym
+sex_tc_dx
+sex_tc_inj_dx
+sex_tc_inj_sn
+sex_tc_next
+sex_tc_next_dx
+sex_tc_next_sn
+sex_tc_push
+sex_tc_push_dx
+sex_tc_push_sn
+sex_tc_refl
+sex_tc_step_dx
+sex_trans
+sex_trans_gen
+sex_trans_id_cfull
+sex_transitive
+sh
+sh_acyclic
+sh_decidable
+sh_lt
+sh_lt_acyclic
+sh_lt_dec
+sh_lt_nexts_inv_lt
+simple
+simple_atom
+simple_dec_ex
+simple_flat
+simple_inv_bind
+simple_inv_bind_aux
+simple_inv_pair
+simple_teqo_repl_dx
+simple_teqo_repl_sn
+sle_seq_trans
+sle_sex_conf
+sle_sex_trans
+Sort
+s_rs_transitive_isid
+s_rs_transitive_lex_inv_isid
+TAtom
+tc_f_dedropable_sn
+tc_f_dropable_dx
+tc_f_dropable_sn
+teqo
+teqo_canc_dx
+teqo_canc_sn
+teqo_dec
+teqo_gref
+teqo_inv_applv_bind_simple
+teqo_inv_gref1
+teqo_inv_gref1_aux
+teqo_inv_lifts_bi
+teqo_inv_lref1
+teqo_inv_lref1_aux
+teqo_inv_pair
+teqo_inv_pair1
+teqo_inv_pair1_aux
+teqo_inv_pair2
+teqo_inv_pair2_aux
+teqo_inv_sort1
+teqo_inv_sort1_aux
+teqo_lifts_bi
+teqo_lifts_dx
+teqo_lifts_sn
+teqo_lref
+teqo_pair
+teqo_refl
+teqo_sort
+teqo_sym
+teqo_trans
+teqx
+teqx_canc_dx
+teqx_canc_sn
+teqx_dec
+teqx_ext
+teqx_feqx
+teqx_fqup_trans
+teqx_fquq_trans
+teqx_fqus_trans
+teqx_fqu_trans
+teqx_fwd_atom1
+teqx_gref
+teqx_inv_gref1
+teqx_inv_gref1_aux
+teqx_inv_lifts_bi
+teqx_inv_lifts_dx
+teqx_inv_lifts_sn
+teqx_inv_lref1
+teqx_inv_lref1_aux
+teqx_inv_pair
+teqx_inv_pair1
+teqx_inv_pair1_aux
+teqx_inv_pair2
+teqx_inv_pair_xy_x
+teqx_inv_pair_xy_y
+teqx_inv_sort1
+teqx_inv_sort1_aux
+teqx_inv_sort2
+teqx_lifts_bi
+teqx_lifts_dx
+teqx_lifts_inv_pair_sn
+teqx_lifts_sn
+teqx_lref
+teqx_pair
+teqx_refl
+teqx_repl
+teqx_reqx_conf
+teqx_reqx_div
+teqx_rex_conf
+teqx_rex_div
+teqx_sort
+teqx_sym
+teqx_teqo
+teqx_tneqx_trans
+teqx_trans
+teqx_tweq
+term
+tneqx_inv_pair
+tneqx_teqx_canc_dx
+TPair
+tw
+tweq
+tweq_abbr
+tweq_abbr_neg
+tweq_abbr_pos
+tweq_abst
+tweq_appl
+tweq_canc_dx
+tweq_canc_sn
+tweq_cast
+tweq_dec
+tweq_fwd_pair_bi
+tweq_fwd_pair_sn
+tweq_gref
+tweq_inv_abbr_neg_sn
+tweq_inv_abbr_pos_bi
+tweq_inv_abbr_pos_sn
+tweq_inv_abbr_pos_x_lifts_y_y
+tweq_inv_abbr_sn
+tweq_inv_abbr_sn_aux
+tweq_inv_abst_sn
+tweq_inv_abst_sn_aux
+tweq_inv_appl_bi
+tweq_inv_appl_sn
+tweq_inv_appl_sn_aux
+tweq_inv_cast_bi
+tweq_inv_cast_sn
+tweq_inv_cast_sn_aux
+tweq_inv_cast_xy_y
+tweq_inv_gref_sn
+tweq_inv_gref_sn_aux
+tweq_inv_lifts_bi
+tweq_inv_lref_sn
+tweq_inv_lref_sn_aux
+tweq_inv_sort_sn
+tweq_inv_sort_sn_aux
+tweq_lifts_bi
+tweq_lifts_dx
+tweq_lifts_sn
+tweq_lref
+tweq_refl
+tweq_repl
+tweq_simple_trans
+tweq_sort
+tweq_sym
+tweq_trans
+tw_le_pair_dx
+tw_pos
+Void
]
qed-.
-theorem drops_conf_div: ∀f1,L,K. ⇩*[Ⓣ,f1] L ≘ K → ∀f2. ⇩*[Ⓣ,f2] L ≘ K →
- 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2.
+theorem drops_conf_div_isuni:
+ ∀f1,L,K. ⇩*[Ⓣ,f1] L ≘ K → ∀f2. ⇩*[Ⓣ,f2] L ≘ K →
+ 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2.
#f1 #L #K #H elim H -f1 -L -K
[ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2
/3 width=1 by isid_inv_eq_repl/
qed-.
(* Basic_2A1: includes: drops_conf_div *)
-lemma drops_conf_div_bind: ∀f1,f2,I1,I2,L,K.
- ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] →
- 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2.
+lemma drops_conf_div_bind_isuni:
+ ∀f1,f2,I1,I2,L,K.
+ ⇩*[Ⓣ,f1] L ≘ K.ⓘ[I1] → ⇩*[Ⓣ,f2] L ≘ K.ⓘ[I2] →
+ 𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2 ∧ I1 = I2.
#f1 #f2 #I1 #I2 #L #K #Hf1 #Hf2 #HU1 #HU2
lapply (drops_isuni_fwd_drop2 … Hf1) // #H1
lapply (drops_isuni_fwd_drop2 … Hf2) // #H2
-lapply (drops_conf_div … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H
+lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H
lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12
lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0
lapply (drops_mono … H0 … Hf2) -L #H
(* Properties with syntactic equivalence on referred entries ****************)
-lemma req_reqx_trans: ∀L1,L,T1. L1 ≡[T1] L →
+lemma req_feqx_trans: ∀L1,L,T1. L1 ≡[T1] L →
∀G1,G2,L2,T2. ❪G1,L,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫.
#L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H
elim (feqx_inv_gen_sn … H) -H #H #HL2 #T12 destruct
#L1 #L2 #H1L #I #T1 #T2 #V
* #n #m #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
-lapply (lveq_inv_bind … H2L) -H2L #HL
+lapply (lveq_inv_bind_O … H2L) -H2L #HL
elim (frees_total L2 V) #g1 #Hg1
elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
lapply (sor_inv_sle_dx … Hg) #H0g
]
qed-.
-lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
+lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
/2 width=4 by lsuba_inv_atom2_aux/ qed-.
fact lsuba_inv_bind2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2. L2 = K2.ⓘ[I] →
(* Advanced inversion lemmas ************************************************)
-lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2.
+lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2.
#I1 #I2 #K1 #K2 #H
elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct //
qed-.
projects / helm.git / commitdiff