include ../Makefile.common
test:
- @./roles.native -C ../.. -r -W > roles.html
+ @./roles.native -C ../.. -r -p
up-css:
@scp roles.css lahar.helm.cs.unibo.it:/projects/helm/public_html/lambdadelta/css/
color: inherit;
}
-/* layouts ******************************************************************/
+/* headings layouts *********************************************************/
+
+.head {
+ font-size: 2em;
+ font-weight: bold;
+ margin: 0.67em 0;
+ text-align: center;
+}
+
+.error {
+ margin-top: 1em;
+}
+
+/* button layouts ***********************************************************/
+
+.buttons {
+ padding-bottom: 1em;
+/* border-bottom: 1px solid black; */
+ margin: 1em 0;
+}
+
+.button {
+ padding: 0.25em 0.5em;
+ border: 1px solid black;
+ margin-right: 1em;
+}
+
+/* status layouts ***********************************************************/
+
+.stage {
+ padding-bottom: 0.75em;
+}
+
+.roles-head {
+ height: 36ex;
+ overflow-y: auto;
+ padding: 1em 0;
+ margin-bottom: 1em;
+ border-bottom: 1px solid black;
+ border-top: 1px solid black;
+}
+
+.role {
+ margin: 0.5em 0.5em;
+ padding: 0.25em 0.25em;
+}
+
+.roles {
+ display: none;
+ border-left: 2em solid white;
+}
+
+.roles:target {
+ display: block;
+}
.atoms-head {
}
-.count {
+.atoms-table {
+ border-spacing: 0.25em;
}
.atoms {
}
.atom {
- padding: 0.25em 0.5em;
+ padding: 0.25em 0.25em;
+}
+
+.count {
}
.selected {
- border: 1pt dotted;
+ border: 1pt solid;
}
/* colors *******************************************************************/
-.object {
- color: skyblue;
+.role-color {
+ color: darkviolet;
+}
+
+.object-color {
+ color: deepskyblue;
+}
+
+.name-color {
+ color: seagreen;
}
-.name {
- color: darkseagreen;
+.error-color {
+ color: red;
}
module WE = WebEngine
let help_B = "<url> Set this base url (default: http://helm.cs.unibo.it/lambdadelta/)"
-let help_C = "<dir> Set this working directory (default: current directory)"
+let help_C = "<dir> Set this relative working directory (default: invocation directory)"
let help_L = " Debug osn lexer"
let help_W = " Run as an LWS application"
let help_X = " Reset all options to defaults"
let help_w = " Save current status"
let help = "Usage: roles [ -LWXamprw | -B <url> | -C <dir> | -os <version> | -t <pointer> | <file> ]*"
+let change_cwd s =
+ EG.cwd := Filename.concat !EG.cwd s
+
let add_tops s =
EE.add_tops (EU.version_of_string s)
let _main = try
Arg.parse [
"-B", Arg.String ((:=) EG.base_url), help_B;
- "-C", Arg.String ((:=) EG.wd), help_C;
+ "-C", Arg.String change_cwd, help_C;
"-L", Arg.Set EG.debug_lexer, help_L;
"-W", Arg.Unit WE.init, help_W;
"-X", Arg.Unit EG.clear, help_X;
let read_waiting fname =
if st.ET.s = [] then EU.raise_error ET.ENoStage else
let ich = Scanf.Scanning.open_in fname in
- let w = EI.read_rev_names ich [] in
+ let ws = EI.read_rev_names ich [] in
Scanf.Scanning.close_in ich;
- st.ET.w <- EU.names_union (List.rev w) st.ET.w
+ let map ws w = EU.names_union ws [w] in
+ st.ET.w <- List.fold_left map st.ET.w ws
let read_status () =
if st.ET.s <> [] then EU.raise_error (ET.EStage st.ET.s) else
- let fname = Filename.concat !EG.wd "roles.osn" in
+ let fname = Filename.concat !EG.cwd "roles.osn" in
let ich = open_in fname in
let tmp = EI.read_status ich in
close_in ich;
st.ET.w <- tmp.ET.w
let write_status () =
- let fname = Filename.concat !EG.wd "roles.osn" in
+ let fname = Filename.concat !EG.cwd "roles.osn" in
let och = open_out fname in
EO.out_status och st;
close_out och
let print_status () =
EO.out_status stdout st
-let visit_status before_t each_t after_t before_w each_w after_w =
- EU.list_visit before_t each_t after_t EU.string_of_obj [1] st.ET.t;
- EU.list_visit before_w each_w after_w EU.string_of_name [2] st.ET.w
+let visit_status
+ before_r each_r before after after_r stage
+ before_t each_t after_t before_w each_w after_w =
+ let visit_tw _ _ = () in
+ let visit_r p r =
+ before (EU.string_of_pointer (List.rev p));
+ EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj (1::p) r.ET.o;
+ EU.list_visit before_w each_w visit_tw after_w EU.string_of_name (2::p) r.ET.n;
+ after ()
+ in
+ EU.list_visit before_r each_r visit_r after_r EU.string_of_role [0] st.ET.r;
+ stage (EU.string_of_version st.ET.s);
+ EU.list_visit before_t each_t visit_tw after_t EU.string_of_obj [1] st.ET.t;
+ EU.list_visit before_w each_w visit_tw after_w EU.string_of_name [2] st.ET.w
val print_status: unit -> unit
val visit_status:
+ (string -> string -> unit) -> (string -> bool -> string -> unit) ->
+ (string -> unit) -> (unit -> unit) -> (unit -> unit) -> (string -> unit) ->
(string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
(string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
unit
let default_base_url = "http://helm.cs.unibo.it/lambdadelta/"
-let default_wd = ""
+let default_cwd = Filename.dirname Sys.argv.(0)
let default_debug_lexer = false
let base_url = ref default_base_url
-let wd = ref default_wd
+let cwd = ref default_cwd
let debug_lexer = ref default_debug_lexer
let clear () =
base_url := default_base_url;
- wd := default_wd;
+ cwd := default_cwd;
debug_lexer := default_debug_lexer
val base_url: string ref
-val wd: string ref
+val cwd: string ref
val debug_lexer: bool ref
| EWrongSelect
| EWrongVersion
| ETops
+ | EWrongRequest of string * string
exception Error of error
ET.r = []; ET.s = []; ET.t = []; ET.w = [];
}
-let string_of_pointer = string_of_version
+let string_of_pointer = string_of_version
let pointer_of_string = version_of_string
-let list_visit before each after string_of p l =
+let list_visit before each visit after string_of p l =
let ptr p = string_of_pointer (List.rev p) in
let rec aux i = function
| [] -> ()
| (b, x)::tl ->
each (ptr (i::p)) b (string_of x);
+ visit (i::p) x;
aux (succ i) tl
in
let s, c = list_count 0 0 l in
after ()
let string_of_error = function
- | ET.EWrongExt x ->
+ | ET.EWrongExt x ->
Printf.sprintf "unknown input file type %S" x
- | ET.EStage v ->
+ | ET.EStage v ->
Printf.sprintf "current stage %S" (string_of_version v)
- | ET.ENoStage ->
+ | ET.ENoStage ->
Printf.sprintf "current stage not defined"
- | ET.EWaiting ->
+ | ET.EWaiting ->
Printf.sprintf "current stage not finished"
- | ET.ENameClash n ->
+ | ET.ENameClash n ->
Printf.sprintf "name clash %S" (string_of_name n)
- | ET.EObjClash o ->
+ | ET.EObjClash o ->
Printf.sprintf "object clash %S" (string_of_obj o)
- | ET.ERoleClash r ->
+ | ET.ERoleClash r ->
Printf.sprintf "role clash %S" (string_of_role r)
- | ET.ENoEntry ->
+ | ET.ENoEntry ->
Printf.sprintf "entry not found"
- | ET.EWrongSelect ->
+ | ET.EWrongSelect ->
Printf.sprintf "selected role is not unique"
- | ET.EWrongVersion ->
+ | ET.EWrongVersion ->
Printf.sprintf "selected role is not in the current stage"
- | ET.ETops ->
+ | ET.ETops ->
Printf.sprintf "top objects already computed"
+ | ET.EWrongRequest (r,a) ->
+ Printf.sprintf "unknown request \"%s=%s\"" r a
val list_select: 'b option -> (bool * 'b) list -> 'b option
val list_visit:
- (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+ (string -> string -> unit) -> (string -> bool -> string -> unit) ->
+ (RolesTypes.pointer -> 'a -> unit) -> (unit -> unit) ->
('a -> string) -> RolesTypes.pointer -> (bool * 'a) list -> unit
val string_of_version: RolesTypes.version -> string
val objs_union: RolesTypes.objs -> RolesTypes.objs -> RolesTypes.objs
+val string_of_role: RolesTypes.role -> string
+
val roles_union: RolesTypes.roles -> RolesTypes.roles -> RolesTypes.roles
val exists_role_deleted: RolesTypes.version -> RolesTypes.roles -> bool
val new_status: RolesTypes.status
+val string_of_pointer: RolesTypes.pointer -> string
+
val pointer_of_string: string -> RolesTypes.pointer
val string_of_error: RolesTypes.error -> string
module KP = Printf
-module EG = RolesGlobal
module EE = RolesEngine
+module EG = RolesGlobal
+module ET = RolesTypes
+module EU = RolesUtils
+module WS = WebLWS
-let open_out_html author description title css icon =
-(*
- YW.open_out "application/xhtml+xml" 0;
-*)
- KP.printf "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n";
- KP.printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n";
- KP.printf "<html xmlns=\"http://www.w3.org/1999/xhtml\" dir=\"ltr\" lang=\"en-us\">\n";
- KP.printf "<head>\n";
- KP.printf " <meta http-equiv=\"Pragma\" content=\"no-cache\"/>\n";
- KP.printf " <meta http-equiv=\"Expires\" content=\"-1\"/>\n";
- KP.printf " <meta http-equiv=\"CACHE-CONTROL\" content=\"NO-CACHE\"/>\n";
- KP.printf " <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/>\n";
- KP.printf " <meta http-equiv=\"Content-Language\" content=\"en-us\"/>\n";
- KP.printf " <meta http-equiv=\"Content-Style-Type\" content=\"text/css\"/>\n";
- KP.printf " <meta name=\"author\" content=\"%s\"/>\n" author;
- KP.printf " <meta name=\"description\" content=\"%s\"/>\n" description;
- KP.printf " <title>%s</title>" title;
- KP.printf " <link rel=\"stylesheet\" type=\"text/css\" href=\"%s\"/>\n" css;
- KP.printf " <link rel=\"shortcut icon\" href=\"%s\"/>\n" icon;
- KP.printf "</head>\n";
- KP.printf "<body lang=\"en-US\">\n"
+let error = ref ""
-let close_out_html () =
- KP.printf "</body>\n";
- KP.printf "</html>\n"
-(*
- YW.close_out ()
-*)
let open_out () =
let author = "λδ development binary: roles manager" in
let description = "λδ development binary: roles manager" in
let title = "Roles Manager" in
let css = Filename.concat !EG.base_url "css/roles.css" in
let icon = Filename.concat !EG.base_url "images/crux_32.ico" in
- open_out_html author description title css icon
+ WS.open_out_html author description title css icon
let close_out () =
- close_out_html ()
+ WS.close_out_html ()
+
+let string_of_request req arg =
+ WS.string_of_request "roles" (["system-"^req, arg], "")
let status_out () =
+ let button_specs = [
+ "default", "Refresh";
+ "save", "Save";
+ "add", "Add";
+ "match", "Match";
+ "remove", "Remove";
+ ] in
+ let each_button (action, str) =
+ let req = string_of_request action "" in
+ KP.printf "<span class=\"button\"><a href=\"%s\">%s</a></span>\n" req str
+ in
+ let before_roles p count =
+ let req = string_of_request "toggle" p in
+ KP.printf "<div class=\"roles-head role-color\">\n";
+ KP.printf "<a href=\"%s\">Roles:</a>\n" req;
+ KP.printf "<span class=\"count\">%s</span>\n" count
+ in
+ let each_role p b str =
+ let req = string_of_request "toggle" p in
+ let s = if b then " selected" else "" in
+ KP.printf "<div class=\"role role-color%s\">" s;
+ KP.printf "<a href=\"#%s\">⮞</a> " p;
+ KP.printf "<a href=\"%s\">%s</a>" req str;
+ KP.printf "</div>\n"
+ in
+ let before_role p =
+ KP.printf "<div id=\"%s\" class=\"roles\">\n" p;
+ in
+ let after_role () =
+ KP.printf "</div>\n"
+ in
+ let after_roles () =
+ KP.printf "</div>\n";
+ KP.printf "<div class=\"buttons\">\n";
+ List.iter each_button button_specs;
+ KP.printf "</div>\n"
+ in
+ let stage s =
+ KP.printf "<div class=\"stage role-color\">";
+ KP.printf "Stage: %s" s;
+ KP.printf "</div>\n"
+ in
let before_atoms a p count =
let c, str =
- if a then "object", "objects"
- else "name", "names"
+ if a then "object-color", "objects"
+ else "name-color", "names"
in
+ let req = string_of_request "toggle" p in
KP.printf "<div class=\"atoms-head %s\">\n" c;
- KP.printf "<a href=\"\">%s:</a>\n" str;
+ KP.printf "<a href=\"%s\">%s:</a>\n" req str;
KP.printf "<span class=\"count\">%s</span>\n" count;
KP.printf "</div>\n";
- KP.printf "<div class=\"atoms\"><table><tr>\n"
+ KP.printf "<div class=\"atoms\"><table class=\"atoms-table\"><tr>\n"
in
let each_atom a p b str =
- let c = if a then "object" else "name" in
+ let c = if a then "object-color" else "name-color" in
let s = if b then " selected" else "" in
- KP.printf "<td class=\"atom %s%s\"><a href=\"\">%s</a></td>\n" c s str
+ let req = string_of_request "toggle" p in
+ KP.printf "<td class=\"atom %s%s\"><a href=\"%s\">%s</a></td>\n" c s req str
in
let after_atoms () =
KP.printf "</tr></table></div>\n"
in
+ KP.printf "<div class=\"head\">Role Manager</div>\n";
EE.visit_status
+ before_roles each_role before_role after_role after_roles stage
(before_atoms true) (each_atom true) after_atoms
- (before_atoms false) (each_atom false) after_atoms
+ (before_atoms false) (each_atom false) after_atoms;
+ if !error <> "" then
+ KP.printf "<div class=\"error error-color\">Error: %s</div>\n" !error
-let init () =
+let handler opt arg () =
+ begin try match opt with
+ | "system-default" -> ()
+ | "system-add" -> EE.add_role ()
+ | "system-remove" -> ()
+ | "system-match" -> EE.add_matching ()
+ | "system-toggle" -> EE.toggle_entry (EU.pointer_of_string arg)
+ | "system-save" -> EE.write_status ()
+ | _ -> EU.raise_error (ET.EWrongRequest (opt, arg))
+ with
+ | ET.Error e -> error := EU.string_of_error e
+ | e -> error := Printexc.to_string e
+ end;
open_out ();
status_out ();
- close_out ()
+ close_out ();
+ error := ""
+
+let init () =
+ WS.loop_in ignore handler ignore ()
--- /dev/null
+(*
+ ||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 KL = List
+module KP = Printf
+module KR = Random
+module KT = String
+
+type request = (string * string) list * string
+
+(* internals *)
+
+let opt_map = function
+ | opt, "" -> opt
+ | opt, arg -> KP.sprintf "%s=%s" opt arg
+
+let get_random () =
+ KP.sprintf "%08X" (KR.bits ())
+
+(* interface *)
+
+let open_out enc len =
+ KP.printf "%s %u\n" enc len
+
+let close_out () =
+ KP.printf "\x04"
+
+let loop_in context handler eot st =
+ let read () = KT.trim (read_line ()) in
+ let rec aux st =
+ let opt = read () in
+ let arg = read () in
+ match opt with
+ | "control-stop" -> st
+ | "control-random" -> aux st
+ | "control-context" -> aux (context st)
+ | "control-eot" -> aux (eot st)
+ | _ ->
+ let st = handler opt arg st in
+ aux st
+ in
+ aux st
+
+let string_of_request cx (opts, fi) =
+ let str =
+ if opts = [] then "" else
+ let opts = ("control-random", get_random ()) :: opts in
+ let str = KT.concat "&" (KL.map opt_map opts) in
+ KP.sprintf "/%s?%s" cx str
+ in
+ KP.sprintf "%s#%s" str fi
+
+let control_input form =
+ KP.printf "<input form=\"%s\" type=\"hidden\" name=\"%s\" value=\"%s\"/>"
+ form "control-random" (get_random ())
+
+let open_out_html author description title css icon =
+ open_out "application/xhtml+xml" 0;
+ KP.printf "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n";
+ KP.printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n";
+ KP.printf "<html xmlns=\"http://www.w3.org/1999/xhtml\" dir=\"ltr\" lang=\"en-us\">\n";
+ KP.printf "<head>\n";
+ KP.printf " <meta http-equiv=\"Pragma\" content=\"no-cache\"/>\n";
+ KP.printf " <meta http-equiv=\"Expires\" content=\"-1\"/>\n";
+ KP.printf " <meta http-equiv=\"CACHE-CONTROL\" content=\"NO-CACHE\"/>\n";
+ KP.printf " <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/>\n";
+ KP.printf " <meta http-equiv=\"Content-Language\" content=\"en-us\"/>\n";
+ KP.printf " <meta http-equiv=\"Content-Style-Type\" content=\"text/css\"/>\n";
+ KP.printf " <meta name=\"author\" content=\"%s\"/>\n" author;
+ KP.printf " <meta name=\"description\" content=\"%s\"/>\n" description;
+ KP.printf " <title>%s</title>" title;
+ KP.printf " <link rel=\"stylesheet\" type=\"text/css\" href=\"%s\"/>\n" css;
+ KP.printf " <link rel=\"shortcut icon\" href=\"%s\"/>\n" icon;
+ KP.printf "</head>\n";
+ KP.printf "<body lang=\"en-US\">\n"
+
+let close_out_html () =
+ KP.printf "</body>\n";
+ KP.printf "</html>\n";
+ close_out ()
--- /dev/null
+(*
+ ||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 request = (string * string) list * string
+
+val open_out: string -> int -> unit
+
+val close_out: unit -> unit
+
+val loop_in: ('a -> 'a) -> (string -> string -> 'a -> 'a) -> ('a -> 'a) -> 'a -> 'a
+
+val string_of_request: string -> request -> string
+
+val control_input: string -> unit
+
+val open_out_html: string -> string -> string -> string -> string -> unit
+
+val close_out_html: unit -> unit
(rel
(ver "1.1")
(old)
- (new "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")
+ (new "A" "AHead" "ASort" "Abbr" "Abst" "Appl" "B" "Bind" "C" "CHead" "CSort" "CTail" "Cast" "F" "Flat" "G" "K" "T" "TApp" "TCons" "THead" "THeads" "TLRef" "TList" "TNil" "TSort" "Void" "abst_dec" "ahead_inj_snd" "aplus" "aplus_ahead_simpl" "aplus_asort_O_simpl" "aplus_asort_le_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" "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" "asucc" "asucc_gen_head" "asucc_gen_sort" "asucc_inj" "asucc_repl" "bind_dec_not" "binder_dec" "c_tail_ind" "cbk" "chead_ctail" "cimp" "cimp_bind" "cimp_flat_dx" "cimp_flat_sx" "cimp_getl_conf" "cle" "cle_flt_trans" "cle_head" "cle_r" "cle_trans_head" "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" "clen" "clt" "clt_cong" "clt_head" "clt_thead" "clt_wf__q_ind" "clt_wf_ind" "cnt" "cnt_head" "cnt_lift" "cnt_sort" "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_drop_conf_O" "csubc_drop_conf_rev" "csubc_drop1_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_S_bind_2" "csubst0_gen_head" "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" "cweight" "dnf_dec" "dnf_dec2" "drop" "drop_S" "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_skip" "drop_skip_bind" "drop_skip_flat" "drop_trans_ge" "drop_trans_le" "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" "ex1__leq_sort_SS" "ex1_arity" "ex1_c" "ex1_t" "ex1_ty3" "ex2_arity" "ex2_c" "ex2_nf2" "ex2_t" "flt" "flt_arith0" "flt_arith1" "flt_arith2" "flt_shift" "flt_thead_dx" "flt_thead_sx" "flt_trans" "flt_wf__q_ind" "flt_wf_ind" "fsubst0" "fsubst0_both" "fsubst0_fst" "fsubst0_gen_base" "fsubst0_snd" "fweight" "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_O" "getl_gen_S" "getl_gen_all" "getl_gen_bind" "getl_gen_flat" "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" "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" "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" "lift_sort" "lift_tle" "lift_tlt_dx" "lift_weight" "lift_weight_add" "lift_weight_add_O" "lift_weight_map" "lift1" "lift1_bind" "lift1_cons_tail" "lift1_flat" "lift1_free" "lift1_lift1" "lift1_lref" "lift1_sort" "lift1_xhg" "lifts" "lifts_inj" "lifts_tapp" "lifts1" "lifts1_cons" "lifts1_flat" "lifts1_nil" "lifts1_xhg" "llt" "llt_head_dx" "llt_head_sx" "llt_repl" "llt_trans" "llt_wf__q_ind" "llt_wf_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__nf2_gen_aux" "nf2_gen_abbr" "nf2_gen_abst" "nf2_gen_beta" "nf2_gen_cast" "nf2_gen_flat" "nf2_gen_lref" "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_S" "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" "s" "s_S" "s_arith0" "s_arith1" "s_inc" "s_inj" "s_le" "s_le_gen" "s_lt" "s_lt_gen" "s_minus" "s_plus" "s_plus_sym" "s_r" "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" "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" "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" "subst_head" "subst_lift_SO" "subst_lref_eq" "subst_lref_gt" "subst_lref_lt" "subst_sort" "subst_subst0" "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_S" "subst1_lift_ge" "subst1_lift_lt" "subst1_refl" "subst1_single" "subst1_subst1" "subst1_subst1_back" "subst1_trans" "tcons_tapp_ex" "term_dec" "terms_props__bind_dec" "terms_props__flat_dec" "terms_props__kind_dec" "thead_x_lift_y_y" "thead_x_y_y" "theads_tapp" "tle" "tle_r" "tlist_ind_rev" "tlt" "tlt_head_dx" "tlt_head_sx" "tlt_trans" "tlt_wf__q_ind" "tlt_wf_ind" "trans" "tslen" "tslt" "tslt_wf__q_ind" "tslt_wf_ind" "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" "wadd" "wadd_O" "wadd_le" "wadd_lt" "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")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/Abbr")
+ (new "Abbr")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/Abst")
+ (new "Abst")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/Appl")
+ (new "Appl")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/Cast")
+ (new "Cast")
)
(rel
(ver "2.1")
(old "1.1/drop")
(new "drop")
)
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_conf_ge")
+ (new "drop_conf_ge")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_conf_lt")
+ (new "drop_conf_lt")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_drop")
+ (new "drop_drop")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_mono")
+ (new "drop_mono")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_refl")
+ (new "drop_refl")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_skip")
+ (new "drop_skip")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_trans_ge")
+ (new "drop_trans_ge")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/drop_trans_le")
+ (new "drop_trans_le")
+ )
(rel
(ver "2.1")
(old "1.1/lift")
(new "lift")
)
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_bind")
+ (new "lift_bind")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_flat")
+ (new "lift_flat")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_inj")
+ (new "lift_inj")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_lref_ge")
+ (new "lift_lref_ge")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_lref_lt")
+ (new "lift_lref_lt")
+ )
+ (rel
+ (ver "2.1")
+ (old "1.1/lift_sort")
+ (new "lift_sort")
+ )
(rel
(ver "2.1")
(old "1.1/lifts")
)
)
(ver "2.1")
- (old "1.1/A" "1.1/Abbr" "1.1/Abst" "1.1/abst_dec" "1.1/AHead" "1.1/ahead_inj_snd" "1.1/aplus" "1.1/aplus_ahead_simpl" "1.1/aplus_asort_le_simpl" "1.1/aplus_asort_O_simpl" "1.1/aplus_asort_simpl" "1.1/aplus_assoc" "1.1/aplus_asucc" "1.1/aplus_asucc_false" "1.1/aplus_gz_ge" "1.1/aplus_gz_le" "1.1/aplus_inj" "1.1/aplus_reg_r" "1.1/aplus_sort_O_S_simpl" "1.1/aplus_sort_S_S_simpl" "1.1/app1" "1.1/Appl" "1.1/aprem" "1.1/aprem_asucc" "1.1/aprem_gen_head_O" "1.1/aprem_gen_head_S" "1.1/aprem_gen_sort" "1.1/aprem_repl" "1.1/aprem_succ" "1.1/aprem_zero" "1.1/arity" "1.1/arity_abbr" "1.1/arity_abst" "1.1/arity_appl" "1.1/arity_appls_abbr" "1.1/arity_appls_appl" "1.1/arity_appls_bind" "1.1/arity_appls_cast" "1.1/arity_aprem" "1.1/arity_bind" "1.1/arity_cast" "1.1/arity_cimp_conf" "1.1/arity_fsubst0" "1.1/arity_gen_abst" "1.1/arity_gen_appl" "1.1/arity_gen_appls" "1.1/arity_gen_bind" "1.1/arity_gen_cast" "1.1/arity_gen_cvoid" "1.1/arity_gen_cvoid_subst0" "1.1/arity_gen_lift" "1.1/arity_gen_lref" "1.1/arity_gen_sort" "1.1/arity_head" "1.1/arity_lift" "1.1/arity_lift1" "1.1/arity_mono" "1.1/arity_nf2_inv_all" "1.1/arity_repellent" "1.1/arity_repl" "1.1/arity_sort" "1.1/arity_sred_pr2" "1.1/arity_sred_pr3" "1.1/arity_sred_wcpr0_pr0" "1.1/arity_sred_wcpr0_pr1" "1.1/arity_subst0" "1.1/ASort" "1.1/asucc" "1.1/asucc_gen_head" "1.1/asucc_gen_sort" "1.1/asucc_inj" "1.1/asucc_repl" "1.1/B" "1.1/Bind" "1.1/bind_dec_not" "1.1/binder_dec" "1.1/C" "1.1/Cast" "1.1/cbk" "1.1/CHead" "1.1/chead_ctail" "1.1/cimp" "1.1/cimp_bind" "1.1/cimp_flat_dx" "1.1/cimp_flat_sx" "1.1/cimp_getl_conf" "1.1/cle" "1.1/clear" "1.1/clear_bind" "1.1/clear_cle" "1.1/clear_clear" "1.1/clear_ctail" "1.1/clear_flat" "1.1/clear_gen_all" "1.1/clear_gen_bind" "1.1/clear_gen_flat" "1.1/clear_gen_flat_r" "1.1/clear_gen_sort" "1.1/clear_getl_trans" "1.1/clear_mono" "1.1/clear_pc3_trans" "1.1/clear_pr2_trans" "1.1/clear_pr3_trans" "1.1/clear_trans" "1.1/clear_wf3_trans" "1.1/cle_flt_trans" "1.1/cle_head" "1.1/clen" "1.1/cle_r" "1.1/cle_trans_head" "1.1/clt" "1.1/clt_cong" "1.1/clt_head" "1.1/clt_thead" "1.1/clt_wf_ind" "1.1/clt_wf__q_ind" "1.1/cnt" "1.1/cnt_head" "1.1/cnt_lift" "1.1/cnt_sort" "1.1/CSort" "1.1/csuba" "1.1/csuba_abst" "1.1/csuba_arity" "1.1/csuba_arity_rev" "1.1/csuba_clear_conf" "1.1/csuba_clear_trans" "1.1/csuba_drop_abbr" "1.1/csuba_drop_abbr_rev" "1.1/csuba_drop_abst" "1.1/csuba_drop_abst_rev" "1.1/csuba_gen_abbr" "1.1/csuba_gen_abbr_rev" "1.1/csuba_gen_abst" "1.1/csuba_gen_abst_rev" "1.1/csuba_gen_bind" "1.1/csuba_gen_bind_rev" "1.1/csuba_gen_flat" "1.1/csuba_gen_flat_rev" "1.1/csuba_gen_void" "1.1/csuba_gen_void_rev" "1.1/csuba_getl_abbr" "1.1/csuba_getl_abbr_rev" "1.1/csuba_getl_abst" "1.1/csuba_getl_abst_rev" "1.1/csuba_head" "1.1/csuba_refl" "1.1/csuba_sort" "1.1/csuba_void" "1.1/csubc" "1.1/csubc_abst" "1.1/csubc_arity_conf" "1.1/csubc_arity_trans" "1.1/csubc_clear_conf" "1.1/csubc_csuba" "1.1/csubc_drop1_conf_rev" "1.1/csubc_drop_conf_O" "1.1/csubc_drop_conf_rev" "1.1/csubc_gen_head_l" "1.1/csubc_gen_head_r" "1.1/csubc_gen_sort_l" "1.1/csubc_gen_sort_r" "1.1/csubc_getl_conf" "1.1/csubc_head" "1.1/csubc_refl" "1.1/csubc_sort" "1.1/csubc_void" "1.1/csubst0" "1.1/csubst0_both" "1.1/csubst0_both_bind" "1.1/csubst0_clear_O" "1.1/csubst0_clear_O_back" "1.1/csubst0_clear_S" "1.1/csubst0_clear_trans" "1.1/csubst0_drop_eq" "1.1/csubst0_drop_eq_back" "1.1/csubst0_drop_gt" "1.1/csubst0_drop_gt_back" "1.1/csubst0_drop_lt" "1.1/csubst0_drop_lt_back" "1.1/csubst0_fst" "1.1/csubst0_fst_bind" "1.1/csubst0_gen_head" "1.1/csubst0_gen_S_bind_2" "1.1/csubst0_gen_sort" "1.1/csubst0_getl_ge" "1.1/csubst0_getl_ge_back" "1.1/csubst0_getl_lt" "1.1/csubst0_getl_lt_back" "1.1/csubst0_snd" "1.1/csubst0_snd_bind" "1.1/csubst1" "1.1/csubst1_bind" "1.1/csubst1_flat" "1.1/csubst1_gen_head" "1.1/csubst1_getl_ge" "1.1/csubst1_getl_ge_back" "1.1/csubst1_getl_lt" "1.1/csubst1_head" "1.1/csubst1_refl" "1.1/csubst1_sing" "1.1/csubt" "1.1/csubt_abst" "1.1/csubt_clear_conf" "1.1/csubt_csuba" "1.1/csubt_drop_abbr" "1.1/csubt_drop_abst" "1.1/csubt_drop_flat" "1.1/csubt_gen_abbr" "1.1/csubt_gen_abst" "1.1/csubt_gen_bind" "1.1/csubt_gen_flat" "1.1/csubt_getl_abbr" "1.1/csubt_getl_abst" "1.1/csubt_head" "1.1/csubt_pc3" "1.1/csubt_pr2" "1.1/csubt_refl" "1.1/csubt_sort" "1.1/csubt_ty3" "1.1/csubt_ty3_ld" "1.1/csubt_void" "1.1/csubv" "1.1/csubv_bind" "1.1/csubv_bind_same" "1.1/csubv_clear_conf" "1.1/csubv_clear_conf_void" "1.1/csubv_drop_conf" "1.1/csubv_flat" "1.1/csubv_getl_conf" "1.1/csubv_getl_conf_void" "1.1/csubv_refl" "1.1/csubv_sort" "1.1/csubv_void" "1.1/CTail" "1.1/c_tail_ind" "1.1/cweight" "1.1/dnf_dec" "1.1/dnf_dec2" "1.1/drop1" "1.1/drop1_cons" "1.1/drop1_cons_tail" "1.1/drop1_csubc_trans" "1.1/drop1_gen_pcons" "1.1/drop1_gen_pnil" "1.1/drop1_getl_trans" "1.1/drop1_nil" "1.1/drop1_skip_bind" "1.1/drop1_trans" "1.1/drop_clear" "1.1/drop_clear_O" "1.1/drop_clear_S" "1.1/drop_conf_ge" "1.1/drop_conf_lt" "1.1/drop_conf_rev" "1.1/drop_csubc_trans" "1.1/drop_ctail" "1.1/drop_drop" "1.1/drop_gen_drop" "1.1/drop_gen_refl" "1.1/drop_gen_skip_l" "1.1/drop_gen_skip_r" "1.1/drop_gen_sort" "1.1/drop_getl_trans_ge" "1.1/drop_getl_trans_le" "1.1/drop_getl_trans_lt" "1.1/drop_mono" "1.1/drop_refl" "1.1/drop_S" "1.1/drop_skip" "1.1/drop_skip_bind" "1.1/drop_skip_flat" "1.1/drop_trans_ge" "1.1/drop_trans_le" "1.1/ex1_arity" "1.1/ex1_c" "1.1/ex1__leq_sort_SS" "1.1/ex1_t" "1.1/ex1_ty3" "1.1/ex2_arity" "1.1/ex2_c" "1.1/ex2_nf2" "1.1/ex2_t" "1.1/F" "1.1/Flat" "1.1/flt" "1.1/flt_arith0" "1.1/flt_arith1" "1.1/flt_arith2" "1.1/flt_shift" "1.1/flt_thead_dx" "1.1/flt_thead_sx" "1.1/flt_trans" "1.1/flt_wf_ind" "1.1/flt_wf__q_ind" "1.1/fsubst0" "1.1/fsubst0_both" "1.1/fsubst0_fst" "1.1/fsubst0_gen_base" "1.1/fsubst0_snd" "1.1/fweight" "1.1/G" "1.1/getl" "1.1/getl_clear_bind" "1.1/getl_clear_conf" "1.1/getl_clear_trans" "1.1/getl_conf_ge_drop" "1.1/getl_conf_le" "1.1/getl_csubst1" "1.1/getl_ctail" "1.1/getl_ctail_clen" "1.1/getl_dec" "1.1/getl_drop" "1.1/getl_drop_conf_ge" "1.1/getl_drop_conf_lt" "1.1/getl_drop_conf_rev" "1.1/getl_drop_trans" "1.1/getl_flat" "1.1/getl_flt" "1.1/getl_gen_2" "1.1/getl_gen_all" "1.1/getl_gen_bind" "1.1/getl_gen_flat" "1.1/getl_gen_O" "1.1/getl_gen_S" "1.1/getl_gen_sort" "1.1/getl_gen_tail" "1.1/getl_head" "1.1/getl_intro" "1.1/getl_mono" "1.1/getl_refl" "1.1/getl_trans" "1.1/getl_wf3_trans" "1.1/gz" "1.1/iso" "1.1/iso_flats_flat_bind_false" "1.1/iso_flats_lref_bind_false" "1.1/iso_gen_head" "1.1/iso_gen_lref" "1.1/iso_gen_sort" "1.1/iso_head" "1.1/iso_lref" "1.1/iso_refl" "1.1/iso_sort" "1.1/iso_trans" "1.1/K" "1.1/leq" "1.1/leq_ahead_asucc_false" "1.1/leq_ahead_false_1" "1.1/leq_ahead_false_2" "1.1/leq_asucc" "1.1/leq_asucc_false" "1.1/leq_eq" "1.1/leq_gen_head1" "1.1/leq_gen_head2" "1.1/leq_gen_sort1" "1.1/leq_gen_sort2" "1.1/leq_head" "1.1/leq_leqz" "1.1/leq_refl" "1.1/leq_sort" "1.1/leq_sym" "1.1/leq_trans" "1.1/leqz" "1.1/leqz_head" "1.1/leqz_leq" "1.1/leqz_sort" "1.1/lift1" "1.1/lift1_bind" "1.1/lift1_cons_tail" "1.1/lift1_flat" "1.1/lift1_free" "1.1/lift1_lift1" "1.1/lift1_lref" "1.1/lift1_sort" "1.1/lift1_xhg" "1.1/lift_bind" "1.1/lift_d" "1.1/lift_flat" "1.1/lift_free" "1.1/lift_free_sym" "1.1/lift_gen_bind" "1.1/lift_gen_flat" "1.1/lift_gen_head" "1.1/lift_gen_lift" "1.1/lift_gen_lref" "1.1/lift_gen_lref_false" "1.1/lift_gen_lref_ge" "1.1/lift_gen_lref_lt" "1.1/lift_gen_sort" "1.1/lift_head" "1.1/lift_inj" "1.1/lift_lref_ge" "1.1/lift_lref_gt" "1.1/lift_lref_lt" "1.1/lift_r" "1.1/lifts1" "1.1/lifts1_cons" "1.1/lifts1_flat" "1.1/lifts1_nil" "1.1/lifts1_xhg" "1.1/lifts_inj" "1.1/lift_sort" "1.1/lifts_tapp" "1.1/lift_tle" "1.1/lift_tlt_dx" "1.1/lift_weight" "1.1/lift_weight_add" "1.1/lift_weight_add_O" "1.1/lift_weight_map" "1.1/llt" "1.1/llt_head_dx" "1.1/llt_head_sx" "1.1/llt_repl" "1.1/llt_trans" "1.1/llt_wf_ind" "1.1/llt_wf__q_ind" "1.1/lref_map" "1.1/lweight" "1.1/lweight_repl" "1.1/minus_s_s" "1.1/mk_G" "1.1/next_plus" "1.1/next_plus_assoc" "1.1/next_plus_gz" "1.1/next_plus_lt" "1.1/next_plus_next" "1.1/nf0_dec" "1.1/nf2" "1.1/nf2_abst" "1.1/nf2_abst_shift" "1.1/nf2_appl_lref" "1.1/nf2_appls_lref" "1.1/nf2_csort_lref" "1.1/nf2_dec" "1.1/nf2_gen_abbr" "1.1/nf2_gen_abst" "1.1/nf2_gen_beta" "1.1/nf2_gen_cast" "1.1/nf2_gen_flat" "1.1/nf2_gen_lref" "1.1/nf2_gen__nf2_gen_aux" "1.1/nf2_gen_void" "1.1/nf2_iso_appls_lref" "1.1/nf2_lift" "1.1/nf2_lift1" "1.1/nf2_lref_abst" "1.1/nf2_pr3_confluence" "1.1/nf2_pr3_unfold" "1.1/nf2_sn3" "1.1/nf2_sort" "1.1/nfs2" "1.1/nfs2_tapp" "1.1/node_inh" "1.1/not_abbr_abst" "1.1/not_abbr_void" "1.1/not_abst_void" "1.1/not_void_abst" "1.1/pc1" "1.1/pc1_head" "1.1/pc1_head_1" "1.1/pc1_head_2" "1.1/pc1_pr0_r" "1.1/pc1_pr0_u" "1.1/pc1_pr0_u2" "1.1/pc1_pr0_x" "1.1/pc1_refl" "1.1/pc1_s" "1.1/pc1_t" "1.1/pc3" "1.1/pc3_abst_dec" "1.1/pc3_dec" "1.1/pc3_eta" "1.1/pc3_fsubst0" "1.1/pc3_gen_abst" "1.1/pc3_gen_abst_shift" "1.1/pc3_gen_appls_lref_abst" "1.1/pc3_gen_appls_lref_sort" "1.1/pc3_gen_appls_sort_abst" "1.1/pc3_gen_cabbr" "1.1/pc3_gen_lift" "1.1/pc3_gen_lift_abst" "1.1/pc3_gen_not_abst" "1.1/pc3_gen_sort" "1.1/pc3_gen_sort_abst" "1.1/pc3_head_1" "1.1/pc3_head_12" "1.1/pc3_head_2" "1.1/pc3_head_21" "1.1/pc3_ind_left" "1.1/pc3_ind_left__pc3_left_pc3" "1.1/pc3_ind_left__pc3_left_pr3" "1.1/pc3_ind_left__pc3_left_sym" "1.1/pc3_ind_left__pc3_left_trans" "1.1/pc3_ind_left__pc3_pc3_left" "1.1/pc3_left" "1.1/pc3_left_r" "1.1/pc3_left_ur" "1.1/pc3_left_ux" "1.1/pc3_lift" "1.1/pc3_nf2" "1.1/pc3_nf2_unfold" "1.1/pc3_pc1" "1.1/pc3_pr0_pr2_t" "1.1/pc3_pr2_fsubst0" "1.1/pc3_pr2_fsubst0_back" "1.1/pc3_pr2_pr2_t" "1.1/pc3_pr2_pr3_t" "1.1/pc3_pr2_r" "1.1/pc3_pr2_u" "1.1/pc3_pr2_u2" "1.1/pc3_pr2_x" "1.1/pc3_pr3_conf" "1.1/pc3_pr3_pc3_t" "1.1/pc3_pr3_r" "1.1/pc3_pr3_t" "1.1/pc3_pr3_x" "1.1/pc3_refl" "1.1/pc3_s" "1.1/pc3_t" "1.1/pc3_thin_dx" "1.1/pc3_wcpr0" "1.1/pc3_wcpr0__pc3_wcpr0_t_aux" "1.1/pc3_wcpr0_t" "1.1/pr0" "1.1/pr0_beta" "1.1/pr0_comp" "1.1/pr0_confluence" "1.1/pr0_confluence__pr0_cong_delta" "1.1/pr0_confluence__pr0_cong_upsilon_cong" "1.1/pr0_confluence__pr0_cong_upsilon_delta" "1.1/pr0_confluence__pr0_cong_upsilon_refl" "1.1/pr0_confluence__pr0_cong_upsilon_zeta" "1.1/pr0_confluence__pr0_delta_delta" "1.1/pr0_confluence__pr0_delta_tau" "1.1/pr0_confluence__pr0_upsilon_upsilon" "1.1/pr0_delta" "1.1/pr0_delta1" "1.1/pr0_gen_abbr" "1.1/pr0_gen_abst" "1.1/pr0_gen_appl" "1.1/pr0_gen_cast" "1.1/pr0_gen_lift" "1.1/pr0_gen_lref" "1.1/pr0_gen_sort" "1.1/pr0_gen_void" "1.1/pr0_lift" "1.1/pr0_refl" "1.1/pr0_subst0" "1.1/pr0_subst0_back" "1.1/pr0_subst0_fwd" "1.1/pr0_subst1" "1.1/pr0_subst1_back" "1.1/pr0_subst1_fwd" "1.1/pr0_tau" "1.1/pr0_upsilon" "1.1/pr0_zeta" "1.1/pr1" "1.1/pr1_comp" "1.1/pr1_confluence" "1.1/pr1_eta" "1.1/pr1_head_1" "1.1/pr1_head_2" "1.1/pr1_pr0" "1.1/pr1_refl" "1.1/pr1_sing" "1.1/pr1_strip" "1.1/pr1_t" "1.1/pr2" "1.1/pr2_cflat" "1.1/pr2_change" "1.1/pr2_confluence" "1.1/pr2_confluence__pr2_delta_delta" "1.1/pr2_confluence__pr2_free_delta" "1.1/pr2_confluence__pr2_free_free" "1.1/pr2_ctail" "1.1/pr2_delta" "1.1/pr2_delta1" "1.1/pr2_free" "1.1/pr2_gen_abbr" "1.1/pr2_gen_abst" "1.1/pr2_gen_appl" "1.1/pr2_gen_cabbr" "1.1/pr2_gen_cast" "1.1/pr2_gen_cbind" "1.1/pr2_gen_cflat" "1.1/pr2_gen_csort" "1.1/pr2_gen_ctail" "1.1/pr2_gen_lift" "1.1/pr2_gen_lref" "1.1/pr2_gen_sort" "1.1/pr2_gen_void" "1.1/pr2_head_1" "1.1/pr2_head_2" "1.1/pr2_lift" "1.1/pr2_subst1" "1.1/pr2_thin_dx" "1.1/pr3" "1.1/pr3_cflat" "1.1/pr3_confluence" "1.1/pr3_eta" "1.1/pr3_flat" "1.1/pr3_gen_abbr" "1.1/pr3_gen_abst" "1.1/pr3_gen_appl" "1.1/pr3_gen_bind" "1.1/pr3_gen_cabbr" "1.1/pr3_gen_cast" "1.1/pr3_gen_lift" "1.1/pr3_gen_lref" "1.1/pr3_gen_sort" "1.1/pr3_gen_void" "1.1/pr3_head_1" "1.1/pr3_head_12" "1.1/pr3_head_2" "1.1/pr3_head_21" "1.1/pr3_iso_appl_bind" "1.1/pr3_iso_appls_abbr" "1.1/pr3_iso_appls_appl_bind" "1.1/pr3_iso_appls_beta" "1.1/pr3_iso_appls_bind" "1.1/pr3_iso_appls_cast" "1.1/pr3_iso_beta" "1.1/pr3_lift" "1.1/pr3_pr0_pr2_t" "1.1/pr3_pr1" "1.1/pr3_pr2" "1.1/pr3_pr2_pr2_t" "1.1/pr3_pr2_pr3_t" "1.1/pr3_pr3_pr3_t" "1.1/pr3_refl" "1.1/pr3_sing" "1.1/pr3_strip" "1.1/pr3_subst1" "1.1/pr3_t" "1.1/pr3_thin_dx" "1.1/pr3_wcpr0_t" "1.1/ptrans" "1.1/r" "1.1/r_arith0" "1.1/r_arith1" "1.1/r_arith2" "1.1/r_arith3" "1.1/r_arith4" "1.1/r_arith5" "1.1/r_arith6" "1.1/r_arith7" "1.1/r_dis" "1.1/r_minus" "1.1/r_plus" "1.1/r_plus_sym" "1.1/r_S" "1.1/s" "1.1/s_arith0" "1.1/s_arith1" "1.1/sc3" "1.1/sc3_abbr" "1.1/sc3_abst" "1.1/sc3_appl" "1.1/sc3_arity" "1.1/sc3_arity_csubc" "1.1/sc3_arity_gen" "1.1/sc3_bind" "1.1/sc3_cast" "1.1/sc3_lift" "1.1/sc3_lift1" "1.1/sc3_props__sc3_sn3_abst" "1.1/sc3_repl" "1.1/sc3_sn3" "1.1/s_inc" "1.1/s_inj" "1.1/s_le" "1.1/s_le_gen" "1.1/s_lt" "1.1/s_lt_gen" "1.1/s_minus" "1.1/sn3" "1.1/sn3_abbr" "1.1/sn3_appl_abbr" "1.1/sn3_appl_appl" "1.1/sn3_appl_appls" "1.1/sn3_appl_beta" "1.1/sn3_appl_bind" "1.1/sn3_appl_cast" "1.1/sn3_appl_lref" "1.1/sn3_appls_abbr" "1.1/sn3_appls_beta" "1.1/sn3_appls_bind" "1.1/sn3_appls_cast" "1.1/sn3_appls_lref" "1.1/sn3_beta" "1.1/sn3_bind" "1.1/sn3_cast" "1.1/sn3_cdelta" "1.1/sn3_cflat" "1.1/sn3_change" "1.1/sn3_cpr3_trans" "1.1/sn3_gen_bind" "1.1/sn3_gen_cflat" "1.1/sn3_gen_def" "1.1/sn3_gen_flat" "1.1/sn3_gen_head" "1.1/sn3_gen_lift" "1.1/sn3_lift" "1.1/sn3_nf2" "1.1/sn3_pr2_intro" "1.1/sn3_pr3_trans" "1.1/sn3_shift" "1.1/sn3_sing" "1.1/sns3" "1.1/sns3_lifts" "1.1/sns3_lifts1" "1.1/s_plus" "1.1/s_plus_sym" "1.1/s_r" "1.1/s_S" "1.1/sty0" "1.1/sty0_abbr" "1.1/sty0_abst" "1.1/sty0_appl" "1.1/sty0_bind" "1.1/sty0_cast" "1.1/sty0_correct" "1.1/sty0_gen_appl" "1.1/sty0_gen_bind" "1.1/sty0_gen_cast" "1.1/sty0_gen_lref" "1.1/sty0_gen_sort" "1.1/sty0_lift" "1.1/sty0_sort" "1.1/sty1" "1.1/sty1_abbr" "1.1/sty1_appl" "1.1/sty1_bind" "1.1/sty1_cast2" "1.1/sty1_cnt" "1.1/sty1_correct" "1.1/sty1_lift" "1.1/sty1_sing" "1.1/sty1_sty0" "1.1/sty1_trans" "1.1/subst" "1.1/subst0" "1.1/subst0_both" "1.1/subst0_confluence_eq" "1.1/subst0_confluence_lift" "1.1/subst0_confluence_neq" "1.1/subst0_fst" "1.1/subst0_gen_head" "1.1/subst0_gen_lift_false" "1.1/subst0_gen_lift_ge" "1.1/subst0_gen_lift_lt" "1.1/subst0_gen_lift_rev_ge" "1.1/subst0_gen_lref" "1.1/subst0_gen_sort" "1.1/subst0_lift_ge" "1.1/subst0_lift_ge_s" "1.1/subst0_lift_ge_S" "1.1/subst0_lift_lt" "1.1/subst0_lref" "1.1/subst0_refl" "1.1/subst0_snd" "1.1/subst0_subst0" "1.1/subst0_subst0_back" "1.1/subst0_tlt" "1.1/subst0_tlt_head" "1.1/subst0_trans" "1.1/subst0_weight_le" "1.1/subst0_weight_lt" "1.1/subst1" "1.1/subst1_confluence_eq" "1.1/subst1_confluence_lift" "1.1/subst1_confluence_neq" "1.1/subst1_ex" "1.1/subst1_gen_head" "1.1/subst1_gen_lift_eq" "1.1/subst1_gen_lift_ge" "1.1/subst1_gen_lift_lt" "1.1/subst1_gen_lref" "1.1/subst1_gen_sort" "1.1/subst1_head" "1.1/subst1_lift_ge" "1.1/subst1_lift_lt" "1.1/subst1_lift_S" "1.1/subst1_refl" "1.1/subst1_single" "1.1/subst1_subst1" "1.1/subst1_subst1_back" "1.1/subst1_trans" "1.1/subst_head" "1.1/subst_lift_SO" "1.1/subst_lref_eq" "1.1/subst_lref_gt" "1.1/subst_lref_lt" "1.1/subst_sort" "1.1/subst_subst0" "1.1/T" "1.1/TApp" "1.1/TCons" "1.1/tcons_tapp_ex" "1.1/term_dec" "1.1/terms_props__bind_dec" "1.1/terms_props__flat_dec" "1.1/terms_props__kind_dec" "1.1/THead" "1.1/THeads" "1.1/theads_tapp" "1.1/thead_x_lift_y_y" "1.1/thead_x_y_y" "1.1/tle" "1.1/tle_r" "1.1/TList" "1.1/tlist_ind_rev" "1.1/TLRef" "1.1/tlt" "1.1/tlt_head_dx" "1.1/tlt_head_sx" "1.1/tlt_trans" "1.1/tlt_wf_ind" "1.1/tlt_wf__q_ind" "1.1/TNil" "1.1/trans" "1.1/tslen" "1.1/tslt" "1.1/tslt_wf_ind" "1.1/tslt_wf__q_ind" "1.1/TSort" "1.1/tweight" "1.1/tweight_lt" "1.1/ty3" "1.1/ty3_abbr" "1.1/ty3_abst" "1.1/ty3_acyclic" "1.1/ty3_appl" "1.1/ty3_arity" "1.1/ty3_bind" "1.1/ty3_cast" "1.1/ty3_conv" "1.1/ty3_correct" "1.1/ty3_cred_pr2" "1.1/ty3_cred_pr3" "1.1/ty3_csubst0" "1.1/ty3_fsubst0" "1.1/ty3_gen_abst_abst" "1.1/ty3_gen_appl" "1.1/ty3_gen_appl_nf2" "1.1/ty3_gen_bind" "1.1/ty3_gen_cabbr" "1.1/ty3_gen_cast" "1.1/ty3_gen_cvoid" "1.1/ty3_gen_lift" "1.1/ty3_gen_lref" "1.1/ty3_gen_sort" "1.1/ty3_getl_subst0" "1.1/ty3_inference" "1.1/ty3_inv_appls_lref_nf2" "1.1/ty3_inv_lref_lref_nf2" "1.1/ty3_inv_lref_nf2" "1.1/ty3_inv_lref_nf2_pc3" "1.1/ty3_lift" "1.1/ty3_nf2_gen__ty3_nf2_inv_abst_aux" "1.1/ty3_nf2_inv_abst" "1.1/ty3_nf2_inv_abst_premise" "1.1/ty3_nf2_inv_abst_premise_csort" "1.1/ty3_nf2_inv_all" "1.1/ty3_nf2_inv_sort" "1.1/ty3_predicative" "1.1/ty3_repellent" "1.1/ty3_sconv" "1.1/ty3_sconv_pc3" "1.1/ty3_shift1" "1.1/ty3_sn3" "1.1/ty3_sort" "1.1/ty3_sred_back" "1.1/ty3_sred_pr0" "1.1/ty3_sred_pr1" "1.1/ty3_sred_pr2" "1.1/ty3_sred_pr3" "1.1/ty3_sred_wcpr0_pr0" "1.1/ty3_sty0" "1.1/ty3_subst0" "1.1/ty3_tred" "1.1/ty3_typecheck" "1.1/ty3_unique" "1.1/tys3" "1.1/tys3_cons" "1.1/tys3_gen_cons" "1.1/tys3_gen_nil" "1.1/tys3_nil" "1.1/Void" "1.1/wadd" "1.1/wadd_le" "1.1/wadd_lt" "1.1/wadd_O" "1.1/wcpr0" "1.1/wcpr0_comp" "1.1/wcpr0_drop" "1.1/wcpr0_drop_back" "1.1/wcpr0_gen_head" "1.1/wcpr0_gen_sort" "1.1/wcpr0_getl" "1.1/wcpr0_getl_back" "1.1/wcpr0_refl" "1.1/weight" "1.1/weight_add_O" "1.1/weight_add_S" "1.1/weight_eq" "1.1/weight_le" "1.1/weight_map" "1.1/wf3" "1.1/wf3_bind" "1.1/wf3_clear_conf" "1.1/wf3_flat" "1.1/wf3_gen_bind1" "1.1/wf3_gen_flat1" "1.1/wf3_gen_head2" "1.1/wf3_gen_sort1" "1.1/wf3_getl_conf" "1.1/wf3_idem" "1.1/wf3_mono" "1.1/wf3_pc3_conf" "1.1/wf3_pr2_conf" "1.1/wf3_pr3_conf" "1.1/wf3_sort" "1.1/wf3_total" "1.1/wf3_ty3" "1.1/wf3_ty3_conf" "1.1/wf3_void")
- (new "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" "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_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_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")
+ (old "1.1/A" "1.1/AHead" "1.1/ASort" "1.1/B" "1.1/Bind" "1.1/C" "1.1/CHead" "1.1/CSort" "1.1/CTail" "1.1/F" "1.1/Flat" "1.1/G" "1.1/K" "1.1/T" "1.1/TApp" "1.1/TCons" "1.1/THead" "1.1/THeads" "1.1/TLRef" "1.1/TList" "1.1/TNil" "1.1/TSort" "1.1/Void" "1.1/abst_dec" "1.1/ahead_inj_snd" "1.1/aplus" "1.1/aplus_ahead_simpl" "1.1/aplus_asort_O_simpl" "1.1/aplus_asort_le_simpl" "1.1/aplus_asort_simpl" "1.1/aplus_assoc" "1.1/aplus_asucc" "1.1/aplus_asucc_false" "1.1/aplus_gz_ge" "1.1/aplus_gz_le" "1.1/aplus_inj" "1.1/aplus_reg_r" "1.1/aplus_sort_O_S_simpl" "1.1/aplus_sort_S_S_simpl" "1.1/app1" "1.1/aprem" "1.1/aprem_asucc" "1.1/aprem_gen_head_O" "1.1/aprem_gen_head_S" "1.1/aprem_gen_sort" "1.1/aprem_repl" "1.1/aprem_succ" "1.1/aprem_zero" "1.1/arity" "1.1/arity_abbr" "1.1/arity_abst" "1.1/arity_appl" "1.1/arity_appls_abbr" "1.1/arity_appls_appl" "1.1/arity_appls_bind" "1.1/arity_appls_cast" "1.1/arity_aprem" "1.1/arity_bind" "1.1/arity_cast" "1.1/arity_cimp_conf" "1.1/arity_fsubst0" "1.1/arity_gen_abst" "1.1/arity_gen_appl" "1.1/arity_gen_appls" "1.1/arity_gen_bind" "1.1/arity_gen_cast" "1.1/arity_gen_cvoid" "1.1/arity_gen_cvoid_subst0" "1.1/arity_gen_lift" "1.1/arity_gen_lref" "1.1/arity_gen_sort" "1.1/arity_head" "1.1/arity_lift" "1.1/arity_lift1" "1.1/arity_mono" "1.1/arity_nf2_inv_all" "1.1/arity_repellent" "1.1/arity_repl" "1.1/arity_sort" "1.1/arity_sred_pr2" "1.1/arity_sred_pr3" "1.1/arity_sred_wcpr0_pr0" "1.1/arity_sred_wcpr0_pr1" "1.1/arity_subst0" "1.1/asucc" "1.1/asucc_gen_head" "1.1/asucc_gen_sort" "1.1/asucc_inj" "1.1/asucc_repl" "1.1/bind_dec_not" "1.1/binder_dec" "1.1/c_tail_ind" "1.1/cbk" "1.1/chead_ctail" "1.1/cimp" "1.1/cimp_bind" "1.1/cimp_flat_dx" "1.1/cimp_flat_sx" "1.1/cimp_getl_conf" "1.1/cle" "1.1/cle_flt_trans" "1.1/cle_head" "1.1/cle_r" "1.1/cle_trans_head" "1.1/clear" "1.1/clear_bind" "1.1/clear_cle" "1.1/clear_clear" "1.1/clear_ctail" "1.1/clear_flat" "1.1/clear_gen_all" "1.1/clear_gen_bind" "1.1/clear_gen_flat" "1.1/clear_gen_flat_r" "1.1/clear_gen_sort" "1.1/clear_getl_trans" "1.1/clear_mono" "1.1/clear_pc3_trans" "1.1/clear_pr2_trans" "1.1/clear_pr3_trans" "1.1/clear_trans" "1.1/clear_wf3_trans" "1.1/clen" "1.1/clt" "1.1/clt_cong" "1.1/clt_head" "1.1/clt_thead" "1.1/clt_wf__q_ind" "1.1/clt_wf_ind" "1.1/cnt" "1.1/cnt_head" "1.1/cnt_lift" "1.1/cnt_sort" "1.1/csuba" "1.1/csuba_abst" "1.1/csuba_arity" "1.1/csuba_arity_rev" "1.1/csuba_clear_conf" "1.1/csuba_clear_trans" "1.1/csuba_drop_abbr" "1.1/csuba_drop_abbr_rev" "1.1/csuba_drop_abst" "1.1/csuba_drop_abst_rev" "1.1/csuba_gen_abbr" "1.1/csuba_gen_abbr_rev" "1.1/csuba_gen_abst" "1.1/csuba_gen_abst_rev" "1.1/csuba_gen_bind" "1.1/csuba_gen_bind_rev" "1.1/csuba_gen_flat" "1.1/csuba_gen_flat_rev" "1.1/csuba_gen_void" "1.1/csuba_gen_void_rev" "1.1/csuba_getl_abbr" "1.1/csuba_getl_abbr_rev" "1.1/csuba_getl_abst" "1.1/csuba_getl_abst_rev" "1.1/csuba_head" "1.1/csuba_refl" "1.1/csuba_sort" "1.1/csuba_void" "1.1/csubc" "1.1/csubc_abst" "1.1/csubc_arity_conf" "1.1/csubc_arity_trans" "1.1/csubc_clear_conf" "1.1/csubc_csuba" "1.1/csubc_drop_conf_O" "1.1/csubc_drop_conf_rev" "1.1/csubc_drop1_conf_rev" "1.1/csubc_gen_head_l" "1.1/csubc_gen_head_r" "1.1/csubc_gen_sort_l" "1.1/csubc_gen_sort_r" "1.1/csubc_getl_conf" "1.1/csubc_head" "1.1/csubc_refl" "1.1/csubc_sort" "1.1/csubc_void" "1.1/csubst0" "1.1/csubst0_both" "1.1/csubst0_both_bind" "1.1/csubst0_clear_O" "1.1/csubst0_clear_O_back" "1.1/csubst0_clear_S" "1.1/csubst0_clear_trans" "1.1/csubst0_drop_eq" "1.1/csubst0_drop_eq_back" "1.1/csubst0_drop_gt" "1.1/csubst0_drop_gt_back" "1.1/csubst0_drop_lt" "1.1/csubst0_drop_lt_back" "1.1/csubst0_fst" "1.1/csubst0_fst_bind" "1.1/csubst0_gen_S_bind_2" "1.1/csubst0_gen_head" "1.1/csubst0_gen_sort" "1.1/csubst0_getl_ge" "1.1/csubst0_getl_ge_back" "1.1/csubst0_getl_lt" "1.1/csubst0_getl_lt_back" "1.1/csubst0_snd" "1.1/csubst0_snd_bind" "1.1/csubst1" "1.1/csubst1_bind" "1.1/csubst1_flat" "1.1/csubst1_gen_head" "1.1/csubst1_getl_ge" "1.1/csubst1_getl_ge_back" "1.1/csubst1_getl_lt" "1.1/csubst1_head" "1.1/csubst1_refl" "1.1/csubst1_sing" "1.1/csubt" "1.1/csubt_abst" "1.1/csubt_clear_conf" "1.1/csubt_csuba" "1.1/csubt_drop_abbr" "1.1/csubt_drop_abst" "1.1/csubt_drop_flat" "1.1/csubt_gen_abbr" "1.1/csubt_gen_abst" "1.1/csubt_gen_bind" "1.1/csubt_gen_flat" "1.1/csubt_getl_abbr" "1.1/csubt_getl_abst" "1.1/csubt_head" "1.1/csubt_pc3" "1.1/csubt_pr2" "1.1/csubt_refl" "1.1/csubt_sort" "1.1/csubt_ty3" "1.1/csubt_ty3_ld" "1.1/csubt_void" "1.1/csubv" "1.1/csubv_bind" "1.1/csubv_bind_same" "1.1/csubv_clear_conf" "1.1/csubv_clear_conf_void" "1.1/csubv_drop_conf" "1.1/csubv_flat" "1.1/csubv_getl_conf" "1.1/csubv_getl_conf_void" "1.1/csubv_refl" "1.1/csubv_sort" "1.1/csubv_void" "1.1/cweight" "1.1/dnf_dec" "1.1/dnf_dec2" "1.1/drop_S" "1.1/drop_clear" "1.1/drop_clear_O" "1.1/drop_clear_S" "1.1/drop_conf_rev" "1.1/drop_csubc_trans" "1.1/drop_ctail" "1.1/drop_gen_drop" "1.1/drop_gen_refl" "1.1/drop_gen_skip_l" "1.1/drop_gen_skip_r" "1.1/drop_gen_sort" "1.1/drop_getl_trans_ge" "1.1/drop_getl_trans_le" "1.1/drop_getl_trans_lt" "1.1/drop_skip_bind" "1.1/drop_skip_flat" "1.1/drop1" "1.1/drop1_cons" "1.1/drop1_cons_tail" "1.1/drop1_csubc_trans" "1.1/drop1_gen_pcons" "1.1/drop1_gen_pnil" "1.1/drop1_getl_trans" "1.1/drop1_nil" "1.1/drop1_skip_bind" "1.1/drop1_trans" "1.1/ex1__leq_sort_SS" "1.1/ex1_arity" "1.1/ex1_c" "1.1/ex1_t" "1.1/ex1_ty3" "1.1/ex2_arity" "1.1/ex2_c" "1.1/ex2_nf2" "1.1/ex2_t" "1.1/flt" "1.1/flt_arith0" "1.1/flt_arith1" "1.1/flt_arith2" "1.1/flt_shift" "1.1/flt_thead_dx" "1.1/flt_thead_sx" "1.1/flt_trans" "1.1/flt_wf__q_ind" "1.1/flt_wf_ind" "1.1/fsubst0" "1.1/fsubst0_both" "1.1/fsubst0_fst" "1.1/fsubst0_gen_base" "1.1/fsubst0_snd" "1.1/fweight" "1.1/getl" "1.1/getl_clear_bind" "1.1/getl_clear_conf" "1.1/getl_clear_trans" "1.1/getl_conf_ge_drop" "1.1/getl_conf_le" "1.1/getl_csubst1" "1.1/getl_ctail" "1.1/getl_ctail_clen" "1.1/getl_dec" "1.1/getl_drop" "1.1/getl_drop_conf_ge" "1.1/getl_drop_conf_lt" "1.1/getl_drop_conf_rev" "1.1/getl_drop_trans" "1.1/getl_flat" "1.1/getl_flt" "1.1/getl_gen_2" "1.1/getl_gen_O" "1.1/getl_gen_S" "1.1/getl_gen_all" "1.1/getl_gen_bind" "1.1/getl_gen_flat" "1.1/getl_gen_sort" "1.1/getl_gen_tail" "1.1/getl_head" "1.1/getl_intro" "1.1/getl_mono" "1.1/getl_refl" "1.1/getl_trans" "1.1/getl_wf3_trans" "1.1/gz" "1.1/iso" "1.1/iso_flats_flat_bind_false" "1.1/iso_flats_lref_bind_false" "1.1/iso_gen_head" "1.1/iso_gen_lref" "1.1/iso_gen_sort" "1.1/iso_head" "1.1/iso_lref" "1.1/iso_refl" "1.1/iso_sort" "1.1/iso_trans" "1.1/leq" "1.1/leq_ahead_asucc_false" "1.1/leq_ahead_false_1" "1.1/leq_ahead_false_2" "1.1/leq_asucc" "1.1/leq_asucc_false" "1.1/leq_eq" "1.1/leq_gen_head1" "1.1/leq_gen_head2" "1.1/leq_gen_sort1" "1.1/leq_gen_sort2" "1.1/leq_head" "1.1/leq_leqz" "1.1/leq_refl" "1.1/leq_sort" "1.1/leq_sym" "1.1/leq_trans" "1.1/leqz" "1.1/leqz_head" "1.1/leqz_leq" "1.1/leqz_sort" "1.1/lift_d" "1.1/lift_free" "1.1/lift_free_sym" "1.1/lift_gen_bind" "1.1/lift_gen_flat" "1.1/lift_gen_head" "1.1/lift_gen_lift" "1.1/lift_gen_lref" "1.1/lift_gen_lref_false" "1.1/lift_gen_lref_ge" "1.1/lift_gen_lref_lt" "1.1/lift_gen_sort" "1.1/lift_head" "1.1/lift_lref_gt" "1.1/lift_r" "1.1/lift_tle" "1.1/lift_tlt_dx" "1.1/lift_weight" "1.1/lift_weight_add" "1.1/lift_weight_add_O" "1.1/lift_weight_map" "1.1/lift1" "1.1/lift1_bind" "1.1/lift1_cons_tail" "1.1/lift1_flat" "1.1/lift1_free" "1.1/lift1_lift1" "1.1/lift1_lref" "1.1/lift1_sort" "1.1/lift1_xhg" "1.1/lifts_inj" "1.1/lifts_tapp" "1.1/lifts1" "1.1/lifts1_cons" "1.1/lifts1_flat" "1.1/lifts1_nil" "1.1/lifts1_xhg" "1.1/llt" "1.1/llt_head_dx" "1.1/llt_head_sx" "1.1/llt_repl" "1.1/llt_trans" "1.1/llt_wf__q_ind" "1.1/llt_wf_ind" "1.1/lref_map" "1.1/lweight" "1.1/lweight_repl" "1.1/minus_s_s" "1.1/mk_G" "1.1/next_plus" "1.1/next_plus_assoc" "1.1/next_plus_gz" "1.1/next_plus_lt" "1.1/next_plus_next" "1.1/nf0_dec" "1.1/nf2" "1.1/nf2_abst" "1.1/nf2_abst_shift" "1.1/nf2_appl_lref" "1.1/nf2_appls_lref" "1.1/nf2_csort_lref" "1.1/nf2_dec" "1.1/nf2_gen__nf2_gen_aux" "1.1/nf2_gen_abbr" "1.1/nf2_gen_abst" "1.1/nf2_gen_beta" "1.1/nf2_gen_cast" "1.1/nf2_gen_flat" "1.1/nf2_gen_lref" "1.1/nf2_gen_void" "1.1/nf2_iso_appls_lref" "1.1/nf2_lift" "1.1/nf2_lift1" "1.1/nf2_lref_abst" "1.1/nf2_pr3_confluence" "1.1/nf2_pr3_unfold" "1.1/nf2_sn3" "1.1/nf2_sort" "1.1/nfs2" "1.1/nfs2_tapp" "1.1/node_inh" "1.1/not_abbr_abst" "1.1/not_abbr_void" "1.1/not_abst_void" "1.1/not_void_abst" "1.1/pc1" "1.1/pc1_head" "1.1/pc1_head_1" "1.1/pc1_head_2" "1.1/pc1_pr0_r" "1.1/pc1_pr0_u" "1.1/pc1_pr0_u2" "1.1/pc1_pr0_x" "1.1/pc1_refl" "1.1/pc1_s" "1.1/pc1_t" "1.1/pc3" "1.1/pc3_abst_dec" "1.1/pc3_dec" "1.1/pc3_eta" "1.1/pc3_fsubst0" "1.1/pc3_gen_abst" "1.1/pc3_gen_abst_shift" "1.1/pc3_gen_appls_lref_abst" "1.1/pc3_gen_appls_lref_sort" "1.1/pc3_gen_appls_sort_abst" "1.1/pc3_gen_cabbr" "1.1/pc3_gen_lift" "1.1/pc3_gen_lift_abst" "1.1/pc3_gen_not_abst" "1.1/pc3_gen_sort" "1.1/pc3_gen_sort_abst" "1.1/pc3_head_1" "1.1/pc3_head_12" "1.1/pc3_head_2" "1.1/pc3_head_21" "1.1/pc3_ind_left" "1.1/pc3_ind_left__pc3_left_pc3" "1.1/pc3_ind_left__pc3_left_pr3" "1.1/pc3_ind_left__pc3_left_sym" "1.1/pc3_ind_left__pc3_left_trans" "1.1/pc3_ind_left__pc3_pc3_left" "1.1/pc3_left" "1.1/pc3_left_r" "1.1/pc3_left_ur" "1.1/pc3_left_ux" "1.1/pc3_lift" "1.1/pc3_nf2" "1.1/pc3_nf2_unfold" "1.1/pc3_pc1" "1.1/pc3_pr0_pr2_t" "1.1/pc3_pr2_fsubst0" "1.1/pc3_pr2_fsubst0_back" "1.1/pc3_pr2_pr2_t" "1.1/pc3_pr2_pr3_t" "1.1/pc3_pr2_r" "1.1/pc3_pr2_u" "1.1/pc3_pr2_u2" "1.1/pc3_pr2_x" "1.1/pc3_pr3_conf" "1.1/pc3_pr3_pc3_t" "1.1/pc3_pr3_r" "1.1/pc3_pr3_t" "1.1/pc3_pr3_x" "1.1/pc3_refl" "1.1/pc3_s" "1.1/pc3_t" "1.1/pc3_thin_dx" "1.1/pc3_wcpr0" "1.1/pc3_wcpr0__pc3_wcpr0_t_aux" "1.1/pc3_wcpr0_t" "1.1/pr0" "1.1/pr0_beta" "1.1/pr0_comp" "1.1/pr0_confluence" "1.1/pr0_confluence__pr0_cong_delta" "1.1/pr0_confluence__pr0_cong_upsilon_cong" "1.1/pr0_confluence__pr0_cong_upsilon_delta" "1.1/pr0_confluence__pr0_cong_upsilon_refl" "1.1/pr0_confluence__pr0_cong_upsilon_zeta" "1.1/pr0_confluence__pr0_delta_delta" "1.1/pr0_confluence__pr0_delta_tau" "1.1/pr0_confluence__pr0_upsilon_upsilon" "1.1/pr0_delta" "1.1/pr0_delta1" "1.1/pr0_gen_abbr" "1.1/pr0_gen_abst" "1.1/pr0_gen_appl" "1.1/pr0_gen_cast" "1.1/pr0_gen_lift" "1.1/pr0_gen_lref" "1.1/pr0_gen_sort" "1.1/pr0_gen_void" "1.1/pr0_lift" "1.1/pr0_refl" "1.1/pr0_subst0" "1.1/pr0_subst0_back" "1.1/pr0_subst0_fwd" "1.1/pr0_subst1" "1.1/pr0_subst1_back" "1.1/pr0_subst1_fwd" "1.1/pr0_tau" "1.1/pr0_upsilon" "1.1/pr0_zeta" "1.1/pr1" "1.1/pr1_comp" "1.1/pr1_confluence" "1.1/pr1_eta" "1.1/pr1_head_1" "1.1/pr1_head_2" "1.1/pr1_pr0" "1.1/pr1_refl" "1.1/pr1_sing" "1.1/pr1_strip" "1.1/pr1_t" "1.1/pr2" "1.1/pr2_cflat" "1.1/pr2_change" "1.1/pr2_confluence" "1.1/pr2_confluence__pr2_delta_delta" "1.1/pr2_confluence__pr2_free_delta" "1.1/pr2_confluence__pr2_free_free" "1.1/pr2_ctail" "1.1/pr2_delta" "1.1/pr2_delta1" "1.1/pr2_free" "1.1/pr2_gen_abbr" "1.1/pr2_gen_abst" "1.1/pr2_gen_appl" "1.1/pr2_gen_cabbr" "1.1/pr2_gen_cast" "1.1/pr2_gen_cbind" "1.1/pr2_gen_cflat" "1.1/pr2_gen_csort" "1.1/pr2_gen_ctail" "1.1/pr2_gen_lift" "1.1/pr2_gen_lref" "1.1/pr2_gen_sort" "1.1/pr2_gen_void" "1.1/pr2_head_1" "1.1/pr2_head_2" "1.1/pr2_lift" "1.1/pr2_subst1" "1.1/pr2_thin_dx" "1.1/pr3" "1.1/pr3_cflat" "1.1/pr3_confluence" "1.1/pr3_eta" "1.1/pr3_flat" "1.1/pr3_gen_abbr" "1.1/pr3_gen_abst" "1.1/pr3_gen_appl" "1.1/pr3_gen_bind" "1.1/pr3_gen_cabbr" "1.1/pr3_gen_cast" "1.1/pr3_gen_lift" "1.1/pr3_gen_lref" "1.1/pr3_gen_sort" "1.1/pr3_gen_void" "1.1/pr3_head_1" "1.1/pr3_head_12" "1.1/pr3_head_2" "1.1/pr3_head_21" "1.1/pr3_iso_appl_bind" "1.1/pr3_iso_appls_abbr" "1.1/pr3_iso_appls_appl_bind" "1.1/pr3_iso_appls_beta" "1.1/pr3_iso_appls_bind" "1.1/pr3_iso_appls_cast" "1.1/pr3_iso_beta" "1.1/pr3_lift" "1.1/pr3_pr0_pr2_t" "1.1/pr3_pr1" "1.1/pr3_pr2" "1.1/pr3_pr2_pr2_t" "1.1/pr3_pr2_pr3_t" "1.1/pr3_pr3_pr3_t" "1.1/pr3_refl" "1.1/pr3_sing" "1.1/pr3_strip" "1.1/pr3_subst1" "1.1/pr3_t" "1.1/pr3_thin_dx" "1.1/pr3_wcpr0_t" "1.1/ptrans" "1.1/r" "1.1/r_S" "1.1/r_arith0" "1.1/r_arith1" "1.1/r_arith2" "1.1/r_arith3" "1.1/r_arith4" "1.1/r_arith5" "1.1/r_arith6" "1.1/r_arith7" "1.1/r_dis" "1.1/r_minus" "1.1/r_plus" "1.1/r_plus_sym" "1.1/s" "1.1/s_S" "1.1/s_arith0" "1.1/s_arith1" "1.1/s_inc" "1.1/s_inj" "1.1/s_le" "1.1/s_le_gen" "1.1/s_lt" "1.1/s_lt_gen" "1.1/s_minus" "1.1/s_plus" "1.1/s_plus_sym" "1.1/s_r" "1.1/sc3" "1.1/sc3_abbr" "1.1/sc3_abst" "1.1/sc3_appl" "1.1/sc3_arity" "1.1/sc3_arity_csubc" "1.1/sc3_arity_gen" "1.1/sc3_bind" "1.1/sc3_cast" "1.1/sc3_lift" "1.1/sc3_lift1" "1.1/sc3_props__sc3_sn3_abst" "1.1/sc3_repl" "1.1/sc3_sn3" "1.1/sn3" "1.1/sn3_abbr" "1.1/sn3_appl_abbr" "1.1/sn3_appl_appl" "1.1/sn3_appl_appls" "1.1/sn3_appl_beta" "1.1/sn3_appl_bind" "1.1/sn3_appl_cast" "1.1/sn3_appl_lref" "1.1/sn3_appls_abbr" "1.1/sn3_appls_beta" "1.1/sn3_appls_bind" "1.1/sn3_appls_cast" "1.1/sn3_appls_lref" "1.1/sn3_beta" "1.1/sn3_bind" "1.1/sn3_cast" "1.1/sn3_cdelta" "1.1/sn3_cflat" "1.1/sn3_change" "1.1/sn3_cpr3_trans" "1.1/sn3_gen_bind" "1.1/sn3_gen_cflat" "1.1/sn3_gen_def" "1.1/sn3_gen_flat" "1.1/sn3_gen_head" "1.1/sn3_gen_lift" "1.1/sn3_lift" "1.1/sn3_nf2" "1.1/sn3_pr2_intro" "1.1/sn3_pr3_trans" "1.1/sn3_shift" "1.1/sn3_sing" "1.1/sns3" "1.1/sns3_lifts" "1.1/sns3_lifts1" "1.1/sty0" "1.1/sty0_abbr" "1.1/sty0_abst" "1.1/sty0_appl" "1.1/sty0_bind" "1.1/sty0_cast" "1.1/sty0_correct" "1.1/sty0_gen_appl" "1.1/sty0_gen_bind" "1.1/sty0_gen_cast" "1.1/sty0_gen_lref" "1.1/sty0_gen_sort" "1.1/sty0_lift" "1.1/sty0_sort" "1.1/sty1" "1.1/sty1_abbr" "1.1/sty1_appl" "1.1/sty1_bind" "1.1/sty1_cast2" "1.1/sty1_cnt" "1.1/sty1_correct" "1.1/sty1_lift" "1.1/sty1_sing" "1.1/sty1_sty0" "1.1/sty1_trans" "1.1/subst" "1.1/subst_head" "1.1/subst_lift_SO" "1.1/subst_lref_eq" "1.1/subst_lref_gt" "1.1/subst_lref_lt" "1.1/subst_sort" "1.1/subst_subst0" "1.1/subst0" "1.1/subst0_both" "1.1/subst0_confluence_eq" "1.1/subst0_confluence_lift" "1.1/subst0_confluence_neq" "1.1/subst0_fst" "1.1/subst0_gen_head" "1.1/subst0_gen_lift_false" "1.1/subst0_gen_lift_ge" "1.1/subst0_gen_lift_lt" "1.1/subst0_gen_lift_rev_ge" "1.1/subst0_gen_lref" "1.1/subst0_gen_sort" "1.1/subst0_lift_ge" "1.1/subst0_lift_ge_S" "1.1/subst0_lift_ge_s" "1.1/subst0_lift_lt" "1.1/subst0_lref" "1.1/subst0_refl" "1.1/subst0_snd" "1.1/subst0_subst0" "1.1/subst0_subst0_back" "1.1/subst0_tlt" "1.1/subst0_tlt_head" "1.1/subst0_trans" "1.1/subst0_weight_le" "1.1/subst0_weight_lt" "1.1/subst1" "1.1/subst1_confluence_eq" "1.1/subst1_confluence_lift" "1.1/subst1_confluence_neq" "1.1/subst1_ex" "1.1/subst1_gen_head" "1.1/subst1_gen_lift_eq" "1.1/subst1_gen_lift_ge" "1.1/subst1_gen_lift_lt" "1.1/subst1_gen_lref" "1.1/subst1_gen_sort" "1.1/subst1_head" "1.1/subst1_lift_S" "1.1/subst1_lift_ge" "1.1/subst1_lift_lt" "1.1/subst1_refl" "1.1/subst1_single" "1.1/subst1_subst1" "1.1/subst1_subst1_back" "1.1/subst1_trans" "1.1/tcons_tapp_ex" "1.1/term_dec" "1.1/terms_props__bind_dec" "1.1/terms_props__flat_dec" "1.1/terms_props__kind_dec" "1.1/thead_x_lift_y_y" "1.1/thead_x_y_y" "1.1/theads_tapp" "1.1/tle" "1.1/tle_r" "1.1/tlist_ind_rev" "1.1/tlt" "1.1/tlt_head_dx" "1.1/tlt_head_sx" "1.1/tlt_trans" "1.1/tlt_wf__q_ind" "1.1/tlt_wf_ind" "1.1/trans" "1.1/tslen" "1.1/tslt" "1.1/tslt_wf__q_ind" "1.1/tslt_wf_ind" "1.1/tweight" "1.1/tweight_lt" "1.1/ty3" "1.1/ty3_abbr" "1.1/ty3_abst" "1.1/ty3_acyclic" "1.1/ty3_appl" "1.1/ty3_arity" "1.1/ty3_bind" "1.1/ty3_cast" "1.1/ty3_conv" "1.1/ty3_correct" "1.1/ty3_cred_pr2" "1.1/ty3_cred_pr3" "1.1/ty3_csubst0" "1.1/ty3_fsubst0" "1.1/ty3_gen_abst_abst" "1.1/ty3_gen_appl" "1.1/ty3_gen_appl_nf2" "1.1/ty3_gen_bind" "1.1/ty3_gen_cabbr" "1.1/ty3_gen_cast" "1.1/ty3_gen_cvoid" "1.1/ty3_gen_lift" "1.1/ty3_gen_lref" "1.1/ty3_gen_sort" "1.1/ty3_getl_subst0" "1.1/ty3_inference" "1.1/ty3_inv_appls_lref_nf2" "1.1/ty3_inv_lref_lref_nf2" "1.1/ty3_inv_lref_nf2" "1.1/ty3_inv_lref_nf2_pc3" "1.1/ty3_lift" "1.1/ty3_nf2_gen__ty3_nf2_inv_abst_aux" "1.1/ty3_nf2_inv_abst" "1.1/ty3_nf2_inv_abst_premise" "1.1/ty3_nf2_inv_abst_premise_csort" "1.1/ty3_nf2_inv_all" "1.1/ty3_nf2_inv_sort" "1.1/ty3_predicative" "1.1/ty3_repellent" "1.1/ty3_sconv" "1.1/ty3_sconv_pc3" "1.1/ty3_shift1" "1.1/ty3_sn3" "1.1/ty3_sort" "1.1/ty3_sred_back" "1.1/ty3_sred_pr0" "1.1/ty3_sred_pr1" "1.1/ty3_sred_pr2" "1.1/ty3_sred_pr3" "1.1/ty3_sred_wcpr0_pr0" "1.1/ty3_sty0" "1.1/ty3_subst0" "1.1/ty3_tred" "1.1/ty3_typecheck" "1.1/ty3_unique" "1.1/tys3" "1.1/tys3_cons" "1.1/tys3_gen_cons" "1.1/tys3_gen_nil" "1.1/tys3_nil" "1.1/wadd" "1.1/wadd_O" "1.1/wadd_le" "1.1/wadd_lt" "1.1/wcpr0" "1.1/wcpr0_comp" "1.1/wcpr0_drop" "1.1/wcpr0_drop_back" "1.1/wcpr0_gen_head" "1.1/wcpr0_gen_sort" "1.1/wcpr0_getl" "1.1/wcpr0_getl_back" "1.1/wcpr0_refl" "1.1/weight" "1.1/weight_add_O" "1.1/weight_add_S" "1.1/weight_eq" "1.1/weight_le" "1.1/weight_map" "1.1/wf3" "1.1/wf3_bind" "1.1/wf3_clear_conf" "1.1/wf3_flat" "1.1/wf3_gen_bind1" "1.1/wf3_gen_flat1" "1.1/wf3_gen_head2" "1.1/wf3_gen_sort1" "1.1/wf3_getl_conf" "1.1/wf3_idem" "1.1/wf3_mono" "1.1/wf3_pc3_conf" "1.1/wf3_pr2_conf" "1.1/wf3_pr3_conf" "1.1/wf3_sort" "1.1/wf3_total" "1.1/wf3_ty3" "1.1/wf3_ty3_conf" "1.1/wf3_void")
+ (new "AAtom" "APair" "ApplDelta" "ApplDelta_lift" "ApplOmega1" "ApplOmega2" "ApplOmega3" "Bind2" "CP0" "CP1" "CP2" "CP3" "Delta" "Delta_lift" "Flat2" "GRef" "IH_da_cpr_lpr" "IH_lstas_cpr_lpr" "IH_snv_cpr_lpr" "IH_snv_lstas" "LAtom" "LPair" "LRef" "Omega1" "Omega2" "S1" "S2" "S3" "S4" "S5" "S6" "S7" "Sort" "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" "TPair" "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" "acr" "acr_aaa" "acr_aaa_csubc_lifts" "acr_abst" "acr_gcr" "append" "append_assoc" "append_atom_sn" "append_inj_dx" "append_inj_sn" "append_inv_pair_dx" "append_inv_refl_dx" "append_length" "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" "candidate" "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" "cpc" "cpc_conf" "cpc_cpcs" "cpc_fwd_cpr" "cpc_refl" "cpc_sym" "cpcs" "cpcs_aaa_mono" "cpcs_bind_dx" "cpcs_bind_sn" "cpcs_bind1" "cpcs_bind2" "cpcs_canc_dx" "cpcs_canc_sn" "cpcs_cpr_conf" "cpcs_cpr_div" "cpcs_cpr_strap1" "cpcs_cpr_strap2" "cpcs_cprs_conf" "cpcs_cprs_div" "cpcs_cprs_dx" "cpcs_cprs_sn" "cpcs_cprs_strap1" "cpcs_cprs_strap2" "cpcs_flat" "cpcs_flat_dx_cpr_rev" "cpcs_ind" "cpcs_ind_dx" "cpcs_inv_abst_dx" "cpcs_inv_abst_sn" "cpcs_inv_abst1" "cpcs_inv_abst2" "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" "cpr" "cpr_ApplOmega_12" "cpr_ApplOmega_23" "cpr_Omega_12" "cpr_Omega_21" "cpr_aaa_conf" "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" "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_pair_sn" "cpr_refl" "cpr_theta" "cpr_zeta" "cpre" "cpre_mono" "cprs" "cprs_aaa_conf" "cprs_beta" "cprs_beta_dx" "cprs_beta_rc" "cprs_bind" "cprs_bind_dx" "cprs_bind2" "cprs_bind2_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" "cpx" "cpx_aaa_conf" "cpx_atom" "cpx_beta" "cpx_bind" "cpx_bind2" "cpx_cpxs" "cpx_ct" "cpx_delift" "cpx_delta" "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" "cpx_st" "cpx_theta" "cpx_zeta" "cpxe" "cpxs" "cpxs_ApplOmega_13" "cpxs_aaa_conf" "cpxs_beta" "cpxs_beta_dx" "cpxs_beta_rc" "cpxs_bind" "cpxs_bind_dx" "cpxs_bind2" "cpxs_bind2_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" "cpxs_theta" "cpxs_theta_dx" "cpxs_theta_rc" "cpxs_trans" "cpxs_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" "cpy_split_down" "cpy_split_up" "cpy_subst" "cpy_trans_down" "cpy_trans_ge" "cpy_weak" "cpy_weak_full" "cpy_weak_top" "cpys" "cpys_antisym_eq" "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_SO2" "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_Y2" "cpys_inv_lref1_drop" "cpys_inv_refl_O2" "cpys_inv_sort1" "cpys_lift_be" "cpys_lift_ge" "cpys_lift_le" "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" "cpys_weak" "cpys_weak_full" "cpys_weak_top" "cpysa" "cpysa_atom" "cpysa_bind" "cpysa_cpy_trans" "cpysa_flat" "cpysa_inv_cpys" "cpysa_refl" "cpysa_subst" "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" "csx_abbr" "csx_abst" "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_cpx_trans" "csx_cpxe" "csx_cpxs_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" "csxa" "csxa_cpxs_trans" "csxa_csx" "csxa_ind" "csxa_intro" "csxa_intro_aux" "csxa_intro_cpx" "csxv" "csxv_inv_cons" "d_appendable_sn" "d_deliftable_sn" "d_deliftable_sn_LTC" "d_deliftable_sn_llstar" "d_liftable" "d_liftable_LTC" "d_liftable_llstar" "d_liftable1" "d_liftables1" "d_liftables1_all" "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" "da_scpds_lpr_aux" "da_scpes_aux" "da_sort" "dedropable_sn" "dedropable_sn_TC" "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" "deg_inv_prec" "deg_inv_pred" "deg_iter" "deg_next_SO" "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" "drop_FT" "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_T" "drop_atom" "drop_conf_be" "drop_conf_div" "drop_conf_le" "drop_drop_lt" "drop_fwd_be" "drop_fwd_drop2" "drop_fwd_length" "drop_fwd_length_eq1" "drop_fwd_length_eq2" "drop_fwd_length_ge" "drop_fwd_length_le_ge" "drop_fwd_length_le_le" "drop_fwd_length_le2" "drop_fwd_length_le4" "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_FT" "drop_inv_FT_aux" "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_T" "drop_inv_atom1" "drop_inv_atom1_aux" "drop_inv_drop1" "drop_inv_drop1_lt" "drop_inv_gen" "drop_inv_length_eq" "drop_inv_pair1" "drop_inv_refl" "drop_inv_skip1" "drop_inv_skip1_aux" "drop_inv_skip2" "drop_inv_skip2_aux" "drop_lpr_trans" "drop_lprs_trans" "drop_lpx_trans" "drop_lpxs_trans" "drop_lsubc_trans" "drop_pair" "drop_refl_atom_O2" "drop_skip_lt" "drop_split" "drop_trans_ge_comm" "drop_trans_lt" "dropable_dx" "dropable_dx_TC" "dropable_sn" "dropable_sn_TC" "drops" "drops_cons" "drops_drop_trans" "drops_inv_cons" "drops_inv_cons_aux" "drops_inv_nil" "drops_inv_nil_aux" "drops_inv_skip2" "drops_lsubc_trans" "drops_nil" "drops_skip" "drops_trans" "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" "fleq" "fleq_canc_dx" "fleq_canc_sn" "fleq_fpb_trans" "fleq_fpbg_trans" "fleq_fpbq" "fleq_fpbs" "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" "fpb_inv_fleq" "fpb_lpx" "fpbg" "fpbg_fleq_trans" "fpbg_fpbq_trans" "fpbg_fpbs_trans" "fpbg_fwd_fpbs" "fpbg_refl" "fpbg_trans" "fpbq" "fpbq_aaa_conf" "fpbq_cpx" "fpbq_fpbg_trans" "fpbq_fpbqa" "fpbq_fpbs" "fpbq_fquq" "fpbq_ind_alt" "fpbq_inv_fpb_alt" "fpbq_lleq" "fpbq_lpx" "fpbq_refl" "fpbqa" "fpbqa_inv_fpbq" "fpbs" "fpbs_aaa_conf" "fpbs_cpx_trans_neq" "fpbs_cpxs_trans" "fpbs_fpb_trans" "fpbs_fpbg" "fpbs_fpbg_trans" "fpbs_fpbsa" "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" "fpbsa" "fpbsa_inv_fpbs" "fqu" "fqu_bind_dx" "fqu_cpr_trans_dx" "fqu_cpr_trans_sn" "fqu_cpx_trans" "fqu_cpx_trans_neq" "fqu_cpxs_trans" "fqu_cpxs_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" "fqu_pair_sn" "fqu_sta_trans" "fqu_wf_ind" "fqup" "fqup_ApplOmega_13" "fqup_bind_dx" "fqup_bind_dx_flat_dx" "fqup_cpx_trans" "fqup_cpx_trans_neq" "fqup_cpxs_trans" "fqup_cpxs_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" "fquq_bind_dx" "fquq_cpr_trans_dx" "fquq_cpr_trans_sn" "fquq_cpx_trans" "fquq_cpx_trans_neq" "fquq_cpxs_trans" "fquq_cpxs_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" "fquqa" "fquqa_drop" "fquqa_inv_fquq" "fquqa_refl" "fqus" "fqus_cpx_trans" "fqus_cpx_trans_neq" "fqus_cpxs_trans" "fqus_cpxs_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" "fqus_trans" "frees" "frees_S" "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_trans" "frees_weak" "fsb" "fsb_fpbs_trans" "fsb_fsba" "fsb_ind_alt" "fsb_ind_fpbg" "fsb_intro" "fsb_inv_csx" "fsba" "fsba_fpbs_trans" "fsba_ind_alt" "fsba_intro" "fsba_inv_fsb" "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" "ib2" "is_lift_dec" "item0" "item2" "lcosx" "lcosx_O" "lcosx_drop_trans_lt" "lcosx_inv_pair" "lcosx_inv_succ" "lcosx_inv_succ_aux" "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_conf_O1" "lift_conf_be" "lift_div_be" "lift_div_le" "lift_fwd_pair1" "lift_fwd_pair2" "lift_fwd_tw" "lift_gref" "lift_inv_O2" "lift_inv_O2_aux" "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_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_minus" "lift_lref_ge_minus_eq" "lift_mono" "lift_refl" "lift_simple_dx" "lift_simple_sn" "lift_split" "lift_total" "lift_trans_be" "lift_trans_ge" "lift_trans_le" "lifts_applv" "lifts_bind" "lifts_cons" "lifts_flat" "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" "lifts_simple_dx" "lifts_simple_sn" "lifts_total" "lifts_trans" "liftsv" "liftsv_cons" "liftsv_liftv_trans_le" "liftsv_nil" "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_Y" "lleq_aaa_trans" "lleq_bind" "lleq_bind_O" "lleq_bind_repl_O" "lleq_bind_repl_SO" "lleq_canc_dx" "lleq_canc_sn" "lleq_cpx_trans" "lleq_cpxs_trans" "lleq_dec" "lleq_flat" "lleq_fpb_trans" "lleq_fpbs" "lleq_fpbs_trans" "lleq_fqu_trans" "lleq_fqup_trans" "lleq_fquq_trans" "lleq_fqus_trans" "lleq_free" "lleq_fwd_bind_O_dx" "lleq_fwd_bind_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_S" "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_lift_ge" "lleq_lift_le" "lleq_llpx_sn_conf" "lleq_llpx_sn_trans" "lleq_lpx_trans" "lleq_lpxs_trans" "lleq_lref" "lleq_lreq_repl" "lleq_lreq_trans" "lleq_nlleq_trans" "lleq_refl" "lleq_skip" "lleq_sort" "lleq_sym" "lleq_trans" "lleq_transitive" "llor" "llor_atom" "llor_skip" "llor_tail_cofrees" "llor_tail_frees" "llor_total" "llpx_sn" "llpx_sn_TC_pair_dx" "llpx_sn_Y" "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_O_dx" "llpx_sn_fwd_bind_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_S" "llpx_sn_inv_S_aux" "llpx_sn_inv_alt_r" "llpx_sn_inv_bind" "llpx_sn_inv_bind_O" "llpx_sn_inv_bind_aux" "llpx_sn_inv_flat" "llpx_sn_inv_flat_aux" "llpx_sn_inv_lift_O" "llpx_sn_inv_lift_be" "llpx_sn_inv_lift_ge" "llpx_sn_inv_lift_le" "llpx_sn_inv_lref_ge_bi" "llpx_sn_inv_lref_ge_dx" "llpx_sn_inv_lref_ge_sn" "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" "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_cpr_trans" "lpr_cprs_conf" "lpr_cprs_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_cpr_trans" "lprs_cprs_conf" "lprs_cprs_conf_dx" "lprs_cprs_conf_sn" "lprs_cprs_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_pair_refl" "lprs_pair2" "lprs_refl" "lprs_strap1" "lprs_strap2" "lprs_strip" "lprs_trans" "lpx" "lpx_aaa_conf" "lpx_cpx_frees_trans" "lpx_cpx_trans" "lpx_cpxs_trans" "lpx_drop_conf" "lpx_drop_trans_O1" "lpx_fqu_trans" "lpx_fqup_trans" "lpx_fquq_trans" "lpx_fqus_trans" "lpx_frees_trans" "lpx_fwd_length" "lpx_inv_atom1" "lpx_inv_atom2" "lpx_inv_pair" "lpx_inv_pair1" "lpx_inv_pair2" "lpx_lleq_fqu_trans" "lpx_lleq_fqup_trans" "lpx_lleq_fquq_trans" "lpx_lleq_fqus_trans" "lpx_lpxs" "lpx_pair" "lpx_refl" "lpx_sn" "lpx_sn_LTC_TC_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_drop_conf" "lpx_sn_drop_trans" "lpx_sn_dropable" "lpx_sn_dropable_aux" "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" "lpx_sn_llpx_sn" "lpx_sn_lpx_sn_alt" "lpx_sn_pair" "lpx_sn_refl" "lpx_sn_trans" "lpx_sn_transitive" "lpxs" "lpxs_aaa_conf" "lpxs_cpx_trans" "lpxs_cpxs_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_fqu_trans" "lpxs_lleq_fqup_trans" "lpxs_lleq_fquq_trans" "lpxs_lleq_fqus_trans" "lpxs_nlleq_inv_step_sn" "lpxs_pair" "lpxs_pair_refl" "lpxs_pair2" "lpxs_refl" "lpxs_strap1" "lpxs_strap2" "lpxs_trans" "lreq" "lreq_O2" "lreq_atom" "lreq_canc_dx" "lreq_canc_sn" "lreq_cpx_trans" "lreq_cpxs_trans" "lreq_drop_conf_be" "lreq_drop_trans_be" "lreq_frees_trans" "lreq_fwd_length" "lreq_inv_O_Y" "lreq_inv_O_Y_aux" "lreq_inv_atom1" "lreq_inv_atom1_aux" "lreq_inv_atom2" "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_lpx_trans_lleq" "lreq_lpx_trans_lleq_aux" "lreq_lpxs_trans_lleq" "lreq_lpxs_trans_lleq_aux" "lreq_pair" "lreq_pair_O_Y" "lreq_pair_lt" "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_O" "lstas_inv_lref1_S" "lstas_inv_lref1_aux" "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_cpr_trans" "lsubr_cprs_trans" "lsubr_cpx_trans" "lsubr_cpxs_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_O2" "lsuby_atom" "lsuby_cpy_trans" "lsuby_cpys_trans" "lsuby_cpysa_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_pair" "lsuby_pair_O_Y" "lsuby_pair_lt" "lsuby_refl" "lsuby_succ" "lsuby_succ_lt" "lsuby_sym" "lsuby_trans" "lsuby_zero" "lsx" "lsx_atom" "lsx_bind" "lsx_bind_lpxs_aux" "lsx_cpx_trans_O" "lsx_cpx_trans_lcosx" "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_lpx_trans" "lsx_lpxs_trans" "lsx_lref_be" "lsx_lref_be_lpxs" "lsx_lref_free" "lsx_lref_skip" "lsx_lreq_conf" "lsx_lsxa" "lsx_sort" "lsxa" "lsxa_ind" "lsxa_intro" "lsxa_intro_aux" "lsxa_intro_lpx" "lsxa_inv_lsx" "lsxa_lleq_trans" "lsxa_lpxs_trans" "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" "pluss" "pluss_inv_cons2" "pluss_inv_nil2" "rfw" "rfw_lpair_dx" "rfw_lpair_sn" "rfw_shift" "rfw_tpair_dx" "rfw_tpair_sn" "ri2" "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_O" "sd_SO" "sd_d" "sd_d_SS" "sd_d_correct" "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" "sta_cprs_scpds" "sta_cpx" "sta_cpx_aux" "sta_fpb" "sta_fpbg" "sta_fpbq" "sta_fpbs" "sta_ldec" "term" "tir_atom" "tix_lref" "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")
)
projects / helm.git / commitdiff