- Authors:
Yannick Forster
Théo Winterhalter
- Files:
Meta-programming using MetaRocq
MetaRocq is a meta-programming framework that reuses the programming language underlying Rocq as meta-programming language.
To follow along, download the MetaRocq prelude
next to this file and compile it with rocq compile MetaRocqPrelude.v.
Notation "$name _" was already used. [notation-overridden,parsing,default]
Notation "_ == _" was already used. [notation-overridden,parsing,default]
For this, MetaRocq has an representation of Rocq terms as an inductive types:
Inductive term : Type :=
tRel : nat -> term
| tVar : ident -> term
| tEvar : nat -> list term -> term
| tSort : sort -> term
| tCast : term -> cast_kind -> term -> term
| tProd : aname -> term -> term -> term
| tLambda : aname -> term -> term -> term
| tLetIn : aname -> term -> term -> term -> term
| tApp : term -> list term -> term
| tConst : kername -> Instance.t -> term
| tInd : inductive -> Instance.t -> term
| tConstruct : inductive -> nat -> Instance.t -> term
| tCase : case_info -> predicate term -> term -> list (branch term) -> term
| tProj : projection -> term -> term
| tFix : mfixpoint term -> nat -> term
| tCoFix : mfixpoint term -> nat -> term
| tInt : PrimInt63.int -> term
| tFloat : PrimFloat.float -> term
| tString : PrimString.string -> term
| tArray : Level.t -> list term -> term -> term -> term.
Arguments tRel n%_nat_scope
Arguments tVar id
Arguments tEvar ev%_nat_scope args%_list_scope
Arguments tSort s
Arguments tCast t kind v
Arguments tProd na ty body
Arguments tLambda na ty body
Arguments tLetIn na def def_ty body
Arguments tApp f args%_list_scope
Arguments tConst c u
Arguments tInd ind u
Arguments tConstruct ind idx%_nat_scope u
Arguments tCase ci type_info discr branches%_list_scope
Arguments tProj proj t
Arguments tFix mfix idx%_nat_scope
Arguments tCoFix mfix idx%_nat_scope
Arguments tInt i
Arguments tFloat f
Arguments tString s
Arguments tArray u arr%_list_scope default type
- No need to understand it all, but you can see how the syntax of Rocq is
encoded. It is actually almost in one-to-one correspondance with the OCaml implementation.
Quoting
The power of MetaRocq is it allows you to go back and forth between this term representation and actual Rocq terms.
We talk about quoting for the action going from actual Rocq definitions to their MetaRocq representation.
Below you see how one can quote the identity function on natural numbers. It starts with a tLam and takes as argument a name for the variable, here "x". Then comes the type of the argument which is a complicated reference to the inductive type nat. Finally the body of the function is tRel 0. This means the 0th variable, in other words the last one to have been introduced, which is x here. This is what we call de Bruijn indices. In fact the "x" annotation is just to help printing, but carries no meaning.
tLam "x"
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat");
inductive_ind := 0
|} [])
(tRel 0)
: term
We can then use $unquote to perform the opposite action.
fun (_ : bool) (x : nat) => x
: bool -> nat -> nat
As we said, you have to use de Bruin indices to deal with variables:
Definition tNat := $quote nat. Definition idNat := $unquote (tLam "x" tNat (tRel 0)).idNat = fun x : nat => x : nat -> nat Arguments idNat x%_nat_scope
Power function
The usual example of meta-programming is the power function. The idea is that mpow 5 x will reduce to (let p := x * x in p * p) * x.
Note: When performing meta-programming, it's safe to deactivate the guard checker locally.
#[bypass_check(guard)] Fixpoint mpow' (n : nat) : term := match n with | 0 => $quote 1 | 1 => tRel 0 | 2 => tApp ($quote mult) [ tRel 0 ; tRel 0 ] | S n' as n => if n mod 2 =? 0 then tLet "p" ($quote nat) (mpow' (div n 2)) (tApp ($quote mult) [ tRel 0 ; tRel 0 ]) else tApp ($quote mult) [ mpow' n' ; tRel 0 ] end.mpow' = fix mpow' (n : nat) : term := match n with | 0 => tApp (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 1 []) [tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []] | 1 => tRel 0 | 2 => tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "mul") []) [tRel 0; tRel 0] | S (S (S _) as n') => if n mod 2 =? 0 then tLet "p" (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []) (mpow' (n / 2)) (tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "mul") []) [tRel 0; tRel 0]) else tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "mul") []) [mpow' n'; tRel 0] end : nat -> term Arguments mpow' n%_nat_scope
See how quoting got expanded at definition time
Definition mpow n := tLam "x" ($quote nat) (mpow' n). Definition pow3 := $unquote (mpow 3).Definition pow5 := $unquote (mpow 5).pow3 = fun x : nat => x * x * x : nat -> nat Arguments pow3 x%_nat_scopeDefinition pow13 := $unquote (mpow 13).pow5 = fun x : nat => (let p := x * x in p * p) * x : nat -> nat Arguments pow5 x%_nat_scopepow13 = fun x : nat => (let p := let p := x * x * x in p * p in p * p) * x : nat -> nat Arguments pow13 x%_nat_scope
Print Assumptions
In Rocq, you have a very useful command which can tell you on which axiom a given lemma depends.
See how it works below.
Axiom LEM : forall (P : Prop), P \/ ~ P. Axiom funext : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g.(fun n : nat => n + 0) = (fun n : nat => n)(fun n : nat => n + 0) = (fun n : nat => n)forall x : nat, x + 0 = xx: natx + 0 = xreflexivity. Qed.x: natx = xFetching opaque proofs from disk for Corelib.Init.PeanoAxioms: funext : forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
Only funext is listed.
We will now try to implement our own Print Assumptions using MetaRocq.
For this, we need to be able to manipulate not only the term but also its
environment to be able to check its dependencies.
For instance, if we inspect foo_ax above, we need to know that funext is
indeed referring to an axiom, and this information is not contained within
foo_ax itself.
We can use $quote_rec to get both the term and its dependencies as follows:
Definition q_foo := $quote_rec foo_ax.q_foo : global_env × term
global_env × term
We can for instance querry the environment to see whether it contains
some constant such as plus_n_O or funext.
Definition foo_env := let (env, _) := q_foo in env.= Some {| cst_type := tPro "n" (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []) (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tRel 0; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tRel 0; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]]); cst_body := Some (tLam "n" (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []) (tApp (tConst (MPfile ["Datatypes"; "Init"; "Corelib"], "nat_ind") []) [tLam "n" (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []) (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tRel 0; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tRel 0; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]]); tCast (tApp (tConstruct {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} 0 []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]) Cast (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]]); tLam "n" (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []) (tLam "IHn" (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tRel 0; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tRel 0; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]]) (tCast (tApp (tConst (MPfile ["Peano"; "Init"; "Corelib"], "f_equal_nat") []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 1 []; tRel 1; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tRel 1; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]; tRel 0]) Cast (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Corelib"], "eq"); inductive_ind := 0 |} []) [tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} []; tApp (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 1 []) [tRel 1]; tApp (tConst (MPfile ["Nat"; "Init"; "Corelib"], "add") []) [tApp (tConstruct {| inductive_mind := (MPfile [ "Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 1 []) [tRel 1]; tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []]]))); tRel 0])); cst_universes := Monomorphic_ctx; cst_relevance := Relevant |} : option constant_body
We get Some and then a big record with a cst_type and cst_body which
is also of the form Some _.
The presence of this cst_body means that this is a Definition and not an
Axiom.
Indeed check out what it returns for funext.
Warning: You have to change tp4 into the name of your file, here this
assumes you didn't rename it and it is tp4.v.
= None
: option constant_body
This time, cst_body := None. It's an axiom.
To give you inspiration for the rest here is the (deep) identity function on
term.
Fixpoint identity (t : term) :=
match t with
| tRel n => tRel n
| tVar id => tVar id
| tEvar ev args => tEvar ev (map identity args)
| tSort s => tSort s
| tCast t kind v => tCast (identity t) kind (identity v)
| tProd na ty body => tProd na (identity ty) (identity body)
| tLambda na ty body => tLambda na (identity ty) (identity body)
| tLetIn na def def_ty body => tLetIn na (identity def) (identity def_ty) (identity body)
| tApp f args => tApp (identity f) (map identity args)
| tConst c u => tConst c u
| tInd ind u => tInd ind u
| tConstruct ind idx u => tConstruct ind idx u
| tCase ind p discr brs =>
let p' := map_predicate id identity identity p in
let brs' := map_branches identity brs in
tCase ind p' (identity discr) brs'
| tProj proj t => tProj proj (identity t)
| tFix mfix idx => tFix (map (map_def identity identity) mfix) idx
| tCoFix mfix idx => tCoFix (map (map_def identity identity) mfix) idx
| tInt i => tInt i
| tFloat f => tFloat f
| tString s => tString s
| tArray u arr def ty => tArray u (map identity arr) (identity def) (identity ty)
end.Exercise: Print Assumptions
Define a Rocq function assumptions : global_env × term -> list kername
such that Compute assumptions ($quote_rec f) returns the list of
assumptions (axioms) that f depends on, including recursively.
Note: You cannot convince Rocq that it is terminating, so we'll deactivate termination checking. That's ok when meta-programming.
Hint: You may use the flat_map and lookup_constant functions too.
Unset Guard Checking.Set Guard Checking. Definition assumptions p := assms p.1 p.2.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]= REPLACE_ME : list kernameDefinition bar_ax : nat := let x := foo_ax in 139.= REPLACE_ME : list kernameModule test.= REPLACE_ME : list kernameP: Prop~ ~ P -> Ptauto. Qed. End test.P: Prop~ ~ P -> PFetching opaque proofs from disk for Stdlib.Logic.Classical_Prop= REPLACE_ME : list kername
Exercise: Folding multiply-add
Define a function which replaces any subterm of the form a * b + c with
muladd a b c defined below.
Hint: You can use u == v to check whether u and v are equal terms
(it returns a boolean).
Definition muladd a b c := a * b + c.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]
Test it with the following.
Transforming terms
We can build terms, but of course we can also inspect them to produce new terms. For this we can build functions that match on the syntax and produce new terms (see exercises). We also provide some utility to do it in a shorter way, altough it might feel more technically involved, we'll let you judge what you prefer.
We'll write a transformation that dupplicates all uses of S inside a term.
Definition double_S :=
transform (fun t k =>
match t with
| tApp s [ n ] =>
if s == $quote S then tApp s [ k t ]
else k t
| _ => k t
end
).transform takes a function that will tell what to do t o the term that deviates from applying the identity function. This function takes as argument a term to inspect t, and a continuation k. Here we do a match on t and look at the only case we find interesting: application of S to some n. If it's not of this form, then we call the continuation on the whole term t so that it does it's job of calling our function on the subterms. When it some S n, we dupplicate the S and then we still call the continuation on t. The reason is that the continuation will not call our program on n if we call k n since it will only call our program on its subterms.
Don't worry if this is a bit hard to get your head around it. It is for me as well!
Let's still look at what it does.
= 20 : nat= 24 : nat
To see clearer, let's not reduce *
= 4 * 6
: nat
We see here, that this operation is really syntactic, and not semantic.
Exercise: Folding multiply-add with transform
Now that you suffered through the definition of fold_muladd, define it again
using transform.
transform takes h : tm_handler and transforms t : term into another
term.
The handler is typically of the form fun t k => ... where t is the subterm
to inspect/transform and k is a continuation. Calling k on a subterm
(or on t) itself, gives control back to transform which will decompose
the subterm once, and then call the handler again on the subsequent subterms.
Definition muladd_handler : tm_handler := REPLACE_ME. Definition fold_muladd_alt := transform muladd_handler.
If you want, you can also do the same for assumptions by using
tm_fold which is similar but implements a fold instead.
Definition assum_fold (env : global_env) : fold_handler (list kername) := REPLACE_ME. Definition assumptions_alt p : list kername := tm_fold (assum_fold p.1) [] p.2.= REPLACE_ME (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat"); inductive_ind := 0 |} 0 []) [] (fun (x : list (modpath × string)) (x0 : term) => match x0 with | tEvar _ args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args x | tCast t _ v => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t) v | tProd _ ty body | tLambda _ ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x ty) body | tLetIn _ def0 def_ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x def0) def_ty) body | tApp f args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f0 args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f0) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f0 args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 (Ffix x1 x2 x5 f0) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x f) | tCase _ type_info discr branches => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list (branch term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) match type_info with | {| pparams := pparams |} => pparams end ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v => Ffix x1 x2 (Ffix x1 x2 x5 t0) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t | tFix mfix _ | tCoFix mfix _ => (fix Ffix (x1 : list (def term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| dtype := dtype |} => dtype end) match x3 with | {| dbody := dbody |} => dbody end) end) mfix x | tArray _ arr default type => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr0 default0 type0 => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr0 x9) default0) type0 | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) arr x) default) type | _ => x end) : list kername= REPLACE_ME (tConst (MPfile ["lesson4_part3"], "foo_ax") []) [] (fun (x : list (modpath × string)) (x0 : term) => match x0 with | tEvar _ args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args x | tCast t _ v => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t) v | tProd _ ty body | tLambda _ ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x ty) body | tLetIn _ def0 def_ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x def0) def_ty) body | tApp f args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f0 args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f0) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f0 args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 (Ffix x1 x2 x5 f0) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x f) | tCase _ type_info discr branches => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list (branch term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) match type_info with | {| pparams := pparams |} => pparams end ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v => Ffix x1 x2 (Ffix x1 x2 x5 t0) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t | tFix mfix _ | tCoFix mfix _ => (fix Ffix (x1 : list (def term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| dtype := dtype |} => dtype end) match x3 with | {| dbody := dbody |} => dbody end) end) mfix x | tArray _ arr default type => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr0 default0 type0 => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr0 x9) default0) type0 | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) arr x) default) type | _ => x end) : list kername= REPLACE_ME (tConst (MPfile ["lesson4_part3"], "bar_ax") []) [] (fun (x : list (modpath × string)) (x0 : term) => match x0 with | tEvar _ args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args x | tCast t _ v => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t) v | tProd _ ty body | tLambda _ ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x ty) body | tLetIn _ def0 def_ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x def0) def_ty) body | tApp f args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f0 args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f0) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f0 args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 (Ffix x1 x2 x5 f0) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x f) | tCase _ type_info discr branches => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list (branch term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) match type_info with | {| pparams := pparams |} => pparams end ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v => Ffix x1 x2 (Ffix x1 x2 x5 t0) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t | tFix mfix _ | tCoFix mfix _ => (fix Ffix (x1 : list (def term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| dtype := dtype |} => dtype end) match x3 with | {| dbody := dbody |} => dbody end) end) mfix x | tArray _ arr default type => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr0 default0 type0 => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr0 x9) default0) type0 | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) arr x) default) type | _ => x end) : list kername= REPLACE_ME (tConst (MPdot (MPfile ["lesson4_part3"]) "test", "DNE") []) [] (fun (x : list (modpath × string)) (x0 : term) => match x0 with | tEvar _ args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args x | tCast t _ v => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v0 => Ffix x1 x2 (Ffix x1 x2 x5 t0) v0 | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t) v | tProd _ ty body | tLambda _ ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty0 body0 | tLambda _ ty0 body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty0) body0 | tLetIn _ def def_ty body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x ty) body | tLetIn _ def0 def_ty body => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body0 | tLambda _ ty body0 => Ffix x1 x2 (Ffix x1 x2 x5 ty) body0 | tLetIn _ def def_ty0 body0 => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty0) body0 | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x def0) def_ty) body | tApp f args => (fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f0 args0 => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args0 (Ffix0 x5 x6 x9 f0) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) args ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f0 args0 => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args0 (Ffix x1 x2 x5 f0) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x f) | tCase _ type_info discr branches => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list (branch term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info0 discr0 branches0 => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) match type_info with | {| pparams := pparams |} => pparams end ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info0 discr0 branches0 => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches0 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info0 with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info0 with | {| preturn := preturn |} => preturn end))) discr0 | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t0 _ v => Ffix x1 x2 (Ffix x1 x2 x5 t0) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t0 => Ffix x1 x2 x5 t0 | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr default type => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr x5) default) type | _ => x5 end)) (list (modpath × string)) REPLACE_ME x t | tFix mfix _ | tCoFix mfix _ => (fix Ffix (x1 : list (def term)) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix0 _ | tCoFix mfix0 _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix0 x9 | tArray _ arr default type => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr x9) default) type | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 match x3 with | {| dtype := dtype |} => dtype end) match x3 with | {| dbody := dbody |} => dbody end) end) mfix x | tArray _ arr default type => (fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : Type) (x2 : term -> x1 -> (x1 -> term -> x1) -> x1) (x3 : x1) (x4 : term) {struct x4} : x1 := x2 x4 x3 (fun (x5 : x1) (x6 : term) => match x6 with | tEvar _ args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args x5 | tCast t _ v => Ffix x1 x2 (Ffix x1 x2 x5 t) v | tProd _ ty body | tLambda _ ty body => Ffix x1 x2 (Ffix x1 x2 x5 ty) body | tLetIn _ def def_ty body => Ffix x1 x2 (Ffix x1 x2 (Ffix x1 x2 x5 def) def_ty) body | tApp f args => (fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) args (Ffix x1 x2 x5 f) | tCase _ type_info discr branches => Ffix x1 x2 ((fix Ffix0 (x7 : list (branch term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 match x9 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix x1 x2 x5 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix x1 x2 x5 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix0 (x7 : list (def term)) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 (Ffix x1 x2 x8 match x9 with | {| dtype := dtype |} => dtype end) match x9 with | {| dbody := dbody |} => dbody end) end) mfix x5 | tArray _ arr0 default0 type0 => Ffix x1 x2 (Ffix x1 x2 ((fix Ffix0 (x7 : list term) (x8 : x1) {struct x7} : x1 := match x7 with | [] => x8 | x9 :: x10 => Ffix0 x10 (Ffix x1 x2 x8 x9) end) arr0 x5) default0) type0 | _ => x5 end)) (list (modpath × string)) REPLACE_ME ((fix Ffix (x1 : list term) (x2 : list (modpath × string)) {struct x1} : list (modpath × string) := match x1 with | [] => x2 | x3 :: x4 => Ffix x4 ((fix Ffix0 (x5 : Type) (x6 : term -> x5 -> (x5 -> term -> x5) -> x5) (x7 : x5) (x8 : term) {struct x8} : x5 := x6 x8 x7 (fun (x9 : x5) (x10 : term) => match x10 with | tEvar _ args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args x9 | tCast t _ v => Ffix0 x5 x6 (Ffix0 x5 x6 x9 t) v | tProd _ ty body | tLambda _ ty body => Ffix0 x5 x6 (Ffix0 x5 x6 x9 ty) body | tLetIn _ def def_ty body => Ffix0 x5 x6 (Ffix0 x5 x6 (Ffix0 x5 x6 x9 def) def_ty) body | tApp f args => (fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) args (Ffix0 x5 x6 x9 f) | tCase _ type_info discr branches => Ffix0 x5 x6 ((fix Ffix1 (x11 : list (branch term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 match x13 with | {| bbody := bbody |} => bbody end) end) branches ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) match type_info with | {| pparams := pparams |} => pparams end (Ffix0 x5 x6 x9 match type_info with | {| preturn := preturn |} => preturn end))) discr | tProj _ t => Ffix0 x5 x6 x9 t | tFix mfix _ | tCoFix mfix _ => (fix Ffix1 (x11 : list (def term)) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 (Ffix0 x5 x6 x12 match x13 with | {| dtype := dtype |} => dtype end) match x13 with | {| dbody := dbody |} => dbody end) end) mfix x9 | tArray _ arr0 default0 type0 => Ffix0 x5 x6 (Ffix0 x5 x6 ((fix Ffix1 (x11 : list term) (x12 : x5) {struct x11} : x5 := match x11 with | [] => x12 | x13 :: x14 => Ffix1 x14 (Ffix0 x5 x6 x12 x13) end) arr0 x9) default0) type0 | _ => x9 end)) (list (modpath × string)) REPLACE_ME x2 x3) end) arr x) default) type | _ => x end) : list kername
Exercise: Reification
Write a command reify that turns a Rocq expression of type nat into an
expression of the following datatype.
Expressions that do not start with + or * are reified as constants.
Inductive arith := | aPlus : arith -> arith -> arith | aTimes : arith -> arith -> arith | aConst : nat -> arith.Not a truly recursive fixpoint. [non-recursive,fixpoints,default]4 * (9 + 12) + (3 + 1 * 7) = 2Admitted.4 * (9 + 12) + (3 + 1 * 7) = 2
Exercise: Instantiating axioms (advanced)
Write a meta-program that takes a definition potentially using an axioms and a proof of said axiom to produce a new definition, equal to the original one expcet that uses of the axioms are replaced by the proof.
The axiom to be replaced is going to be given as a kername, like those
collected by assumptions.
You don't actually have to verify that the constant is indeed an axiom.
Hint: You will need eq_constant.
Definition instantiate_axiom (ax : kername) (prf : term) : term -> term := REPLACE_ME. Axiom mystery : nat. Definition what := mystery * 3.
Exercise: Removing axioms (advanced)
A slightly harder version would be to turn a definition using axioms to one assuming these axioms with an implication.
For instance, for the foo_ax defined above which uses funext, we would
expect something of the following type:
(forall A B (f g : A -> B), (forall x, f x = g x) -> f = g) -> (fun n => n + 0) = (fun n => n)
Hint: You can use assumptions and lookup_constant to get the type of a
constant, and lift0 1 t to weaken t by adding one new variable in the
context.
You can also use a variant of transform called transform_nb which also
tracks the number of introduced variables (to know how much to lift by).
Definition unaxiom (p : global_env * term) : term := REPLACE_ME. Axiom unkown : bool. Axiom random : nat -> nat. Definition test f := if unkown then what else random (f 9).