diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index b2874e9b..0dd89943 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -894,6 +894,8 @@ Axiom atBVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n
 
 Axiom at_gen_BVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (a : Type), forall (f : forall (i : @bitvector n), @is_bvult n i len -> a), forall (ix : @bitvector n), forall (pf : @is_bvult n ix len), @SAWCoreScaffolding.EqP a (@atBVVec n len a (@genBVVec n len a f) ix pf) (f ix pf) .
 
+Axiom gen_at_BVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (a : Type), forall (x : @BVVec n len a), @SAWCoreScaffolding.EqP (@BVVec n len a) (@genBVVec n len a (@atBVVec n len a x)) x .
+
 Definition updBVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (a : Type), @BVVec n len a -> forall (ix : @bitvector n), @is_bvult n ix len -> a -> @BVVec n len a :=
   fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (a : Type) (v : @BVVec n len a) (ix : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (pf : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n ix len) (@SAWCoreScaffolding.true)) (elem : a) => @genBVVec n len a (fun (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true)) => if @bvEq n i ix then elem else @atBVVec n len a v ix pf).
 
@@ -969,14 +971,15 @@ Inductive IRTDesc (As : @ListSort) : Type :=
 | IRT_mu : @IRTDesc As -> @IRTDesc As
 | IRT_Either : @IRTDesc As -> @IRTDesc As -> @IRTDesc As
 | IRT_prod : @IRTDesc As -> @IRTDesc As -> @IRTDesc As
-| IRT_sigT : forall (n : @SAWCoreScaffolding.Nat), (@listSortGet As n -> @IRTDesc As) -> @IRTDesc As
+| IRT_sigT : forall (i : @SAWCoreScaffolding.Nat), (@listSortGet As i -> @IRTDesc As) -> @IRTDesc As
+| IRT_BVVec : forall (n : @SAWCoreScaffolding.Nat), @bitvector n -> forall (D : @IRTDesc As), @IRTDesc As
 | IRT_unit :  @IRTDesc As
 | IRT_empty :  @IRTDesc As
-| IRT_varT : @SAWCoreScaffolding.Nat -> @IRTDesc As
+| IRT_varT : forall (i : @SAWCoreScaffolding.Nat), @IRTDesc As
 .
 
-Definition IRTDesc__rec : forall (As : @ListSort), forall (P : @IRTDesc As -> Type), (forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varD As n)) -> (forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) -> (forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), (forall (a : @listSortGet As n), P (Df a)) -> P (@IRT_sigT As n Df)) -> P (@IRT_unit As) -> P (@IRT_empty As) -> (forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varT As n)) -> forall (D : @IRTDesc As), P D :=
-  fun (As : @ListSort) (P : @IRTDesc As -> Type) (f1 : forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varD As n)) (f2 : forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) (f3 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) (f4 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) (f5 : forall (n : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As), (forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), P (Df a)) -> P (@IRT_sigT As n Df)) (f6 : P (@IRT_unit As)) (f7 : P (@IRT_empty As)) (f8 : forall (n : @SAWCoreScaffolding.Nat), P (@IRT_varT As n)) (D : @IRTDesc As) => SAWCorePrelude.IRTDesc_rect As P f1 f2 f3 f4 f5 f6 f7 f8 D.
+Definition IRTDesc__rec : forall (As : @ListSort), forall (P : @IRTDesc As -> Type), (forall (i : @SAWCoreScaffolding.Nat), P (@IRT_varD As i)) -> (forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) -> (forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) -> (forall (i : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As i -> @IRTDesc As), (forall (a : @listSortGet As i), P (Df a)) -> P (@IRT_sigT As i Df)) -> (forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (D : @IRTDesc As), P D -> P (@IRT_BVVec As n len D)) -> P (@IRT_unit As) -> P (@IRT_empty As) -> (forall (i : @SAWCoreScaffolding.Nat), P (@IRT_varT As i)) -> forall (D : @IRTDesc As), P D :=
+  fun (As : @ListSort) (P : @IRTDesc As -> Type) (f1 : forall (i : @SAWCoreScaffolding.Nat), P (@IRT_varD As i)) (f2 : forall (D : @IRTDesc As), P D -> P (@IRT_mu As D)) (f3 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_Either As Dl Dr)) (f4 : forall (Dl : @IRTDesc As), P Dl -> forall (Dr : @IRTDesc As), P Dr -> P (@IRT_prod As Dl Dr)) (f5 : forall (i : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As), (forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i), P (Df a)) -> P (@IRT_sigT As i Df)) (f6 : forall (n : @SAWCoreScaffolding.Nat), forall (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (D : @IRTDesc As), P D -> P (@IRT_BVVec As n len D)) (f7 : P (@IRT_unit As)) (f8 : P (@IRT_empty As)) (f9 : forall (i : @SAWCoreScaffolding.Nat), P (@IRT_varT As i)) (D : @IRTDesc As) => SAWCorePrelude.IRTDesc_rect As P f1 f2 f3 f4 f5 f6 f7 f8 f9 D.
 
 Inductive IRTSubsts (As : @ListSort) : Type :=
 | IRTs_Nil :  @IRTSubsts As
@@ -993,27 +996,30 @@ Definition dropIRTs : forall (As : @ListSort), @IRTSubsts As -> @SAWCoreScaffold
   fun (As : @ListSort) => @IRTSubsts__rec As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n)).
 
 Inductive IRT (As : @ListSort) : forall (_1 : @IRTSubsts As), forall (_2 : @IRTDesc As), Type :=
-| IRT_elemD : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) -> @IRT As Ds (@IRT_varD As n)
+| IRT_elemD : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds i) -> @IRT As Ds (@IRT_varD As i)
 | IRT_fold : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D -> @IRT As Ds (@IRT_mu As D)
 | IRT_Left : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dl -> @IRT As Ds (@IRT_Either As Dl Dr)
 | IRT_Right : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dr -> @IRT As Ds (@IRT_Either As Dl Dr)
 | IRT_pair : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), @IRT As Ds Dl -> @IRT As Ds Dr -> @IRT As Ds (@IRT_prod As Dl Dr)
-| IRT_existT : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), forall (a : @listSortGet As n), @IRT As Ds (Df a) -> @IRT As Ds (@IRT_sigT As n Df)
+| IRT_existT : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As i -> @IRTDesc As), forall (a : @listSortGet As i), @IRT As Ds (Df a) -> @IRT As Ds (@IRT_sigT As i Df)
+| IRT_genBVVec : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (D : @IRTDesc As), (forall (i : @bitvector n), @is_bvult n i len -> @IRT As Ds D) -> @IRT As Ds (@IRT_BVVec As n len D)
 | IRT_tt : forall (Ds : @IRTSubsts As), @IRT As Ds (@IRT_unit As)
-| IRT_elemT : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), @listSortGet As n -> @IRT As Ds (@IRT_varT As n)
+| IRT_elemT : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), @listSortGet As i -> @IRT As Ds (@IRT_varT As i)
 .
 
-Definition IRT__rec : forall (As : @ListSort), forall (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type), (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (x : @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) x -> P Ds (@IRT_varD As n) (@IRT_elemD As Ds n x)) -> (forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) -> (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As n -> @IRTDesc As), forall (a : @listSortGet As n), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As n Df) (@IRT_existT As Ds n Df a xf)) -> (forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) -> (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (a : @listSortGet As n), P Ds (@IRT_varT As n) (@IRT_elemT As Ds n a)) -> forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As Ds D), P Ds D x :=
-  fun (As : @ListSort) (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type) (f1 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds n) x -> P Ds (@IRT_varD As n) (@IRT_elemD As Ds n x)) (f2 : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) (f3 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) (f4 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) (f5 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) (f6 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As n Df) (@IRT_existT As Ds n Df a xf)) (f7 : forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) (f8 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), P Ds (@IRT_varT As n) (@IRT_elemT As Ds n a)) (Ds : @IRTSubsts As) (D : @IRTDesc As) (x : @IRT As Ds D) => SAWCorePrelude.IRT_rect As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x.
+Definition IRT__rec : forall (As : @ListSort), forall (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type), (forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (x : @IRT As (@dropIRTs As Ds (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds i)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds i) x -> P Ds (@IRT_varD As i) (@IRT_elemD As Ds i x)) -> (forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) -> (forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) -> (forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (Df : @listSortGet As i -> @IRTDesc As), forall (a : @listSortGet As i), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As i Df) (@IRT_existT As Ds i Df a xf)) -> (forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (len : @bitvector n), forall (D : @IRTDesc As), forall (xg : forall (i : @bitvector n), @is_bvult n i len -> @IRT As Ds D), (forall (i : @bitvector n), forall (pf : @is_bvult n i len), P Ds D (xg i pf)) -> P Ds (@IRT_BVVec As n len D) (@IRT_genBVVec As Ds n len D xg)) -> (forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) -> (forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (a : @listSortGet As i), P Ds (@IRT_varT As i) (@IRT_elemT As Ds i a)) -> forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As Ds D), P Ds D x :=
+  fun (As : @ListSort) (P : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> Type) (f1 : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n)) Ds (@SAWCoreScaffolding.Succ i)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n)) Ds i)), P (@dropIRTs As Ds (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds i) x -> P Ds (@IRT_varD As i) (@IRT_elemD As Ds i x)) (f2 : forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), forall (x : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D), P (@IRTs_Cons As (@IRT_mu As D) Ds) D x -> P Ds (@IRT_mu As D) (@IRT_fold As Ds D x)) (f3 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> P Ds (@IRT_Either As Dl Dr) (@IRT_Left As Ds Dl Dr xl)) (f4 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_Either As Dl Dr) (@IRT_Right As Ds Dl Dr xr)) (f5 : forall (Ds : @IRTSubsts As), forall (Dl : @IRTDesc As), forall (Dr : @IRTDesc As), forall (xl : @IRT As Ds Dl), P Ds Dl xl -> forall (xr : @IRT As Ds Dr), P Ds Dr xr -> P Ds (@IRT_prod As Dl Dr) (@IRT_pair As Ds Dl Dr xl xr)) (f6 : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i), forall (xf : @IRT As Ds (Df a)), P Ds (Df a) xf -> P Ds (@IRT_sigT As i Df) (@IRT_existT As Ds i Df a xf)) (f7 : forall (Ds : @IRTSubsts As), forall (n : @SAWCoreScaffolding.Nat), forall (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (D : @IRTDesc As), forall (xg : forall (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true) -> @IRT As Ds D), (forall (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (pf : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true)), P Ds D (xg i pf)) -> P Ds (@IRT_BVVec As n len D) (@IRT_genBVVec As Ds n len D xg)) (f8 : forall (Ds : @IRTSubsts As), P Ds (@IRT_unit As) (@IRT_tt As Ds)) (f9 : forall (Ds : @IRTSubsts As), forall (i : @SAWCoreScaffolding.Nat), forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i), P Ds (@IRT_varT As i) (@IRT_elemT As Ds i a)) (Ds : @IRTSubsts As) (D : @IRTDesc As) (x : @IRT As Ds D) => SAWCorePrelude.IRT_rect As P f1 f2 f3 f4 f5 f6 f7 f8 f9 Ds D x.
 
 Definition UnfoldedIRT : forall (As : @ListSort), @IRTSubsts As -> @IRTDesc As -> Type :=
-  fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D Ds.
+  fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) D Ds.
 
 Definition unfoldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @IRT As Ds D -> @UnfoldedIRT As Ds D :=
-  fun (As : @ListSort) => @IRT__rec As (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As Ds D) => @UnfoldedIRT As Ds D) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n)) (_1 : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds1 n1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf a Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds n) (@dropIRTs As Ds (@SAWCoreScaffolding.Succ n))) => x) (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D) (rec : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) D (@IRTs_Cons As (@IRT_mu As D) Ds)) => rec) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dl Ds) => @Left (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recl) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dr Ds) => @Right (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recr) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n) Dl Ds) (_2 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_3 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds1 n)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl1 Ds1) (recr Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl1 Ds1) (recr Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (_3 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As n) => recf a Ds1)) (fun (_3 : @IRTSubsts As) => unit) (fun (_3 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_3 : @IRTSubsts As) => @listSortGet As n) Dr Ds) => pair recl recr) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (_1 : @IRT As Ds (Df a)) (recf : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds1 n1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n2)) As n1) => recf a1 Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds) => @existT (@listSortGet As n) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds (Df a1)) a recf) (fun (Ds : @IRTSubsts As) => tt) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => a).
+  fun (As : @ListSort) => @IRT__rec As (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As Ds D) => @UnfoldedIRT As Ds D) (fun (Ds : @IRTSubsts As) (i : @SAWCoreScaffolding.Nat) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds1 (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n)) Ds (@SAWCoreScaffolding.Succ i)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n)) Ds i)) (_1 : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i1)) (@atIRTs As Ds1 i1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i1) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i1) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n)) Ds i) (@dropIRTs As Ds (@SAWCoreScaffolding.Succ i))) => x) (fun (Ds : @IRTSubsts As) (D : @IRTDesc As) (_1 : @IRT As (@IRTs_Cons As (@IRT_mu As D) Ds) D) (rec : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As i) D (@IRTs_Cons As (@IRT_mu As D) Ds)) => rec) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As i) Dl Ds) => @Left (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recl) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As i) Dr Ds) => @Right (@UnfoldedIRT As Ds Dl) (@UnfoldedIRT As Ds Dr) recr) (fun (Ds : @IRTSubsts As) (Dl : @IRTDesc As) (Dr : @IRTDesc As) (_1 : @IRT As Ds Dl) (recl : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As i) Dl Ds) (_2 : @IRT As Ds Dr) (recr : SAWCorePrelude.IRTDesc_rect As (fun (_3 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds1 i)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl1 Ds1) (recr Ds1)) (fun (_3 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl1 Ds1) (recr Ds1)) (fun (i : @SAWCoreScaffolding.Nat) (_3 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n)) As i) => recf a Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_3 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_3 : @IRTSubsts As) => unit) (fun (_3 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_3 : @IRTSubsts As) => @listSortGet As i) Dr Ds) => pair recl recr) (fun (Ds : @IRTSubsts As) (i : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) (_1 : @IRT As Ds (Df a)) (recf : SAWCorePrelude.IRTDesc_rect As (fun (_2 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i1)) (@atIRTs As Ds1 i1)) (fun (D : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D) Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_2 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_3 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i1 : @SAWCoreScaffolding.Nat) (_2 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n)) As i1) => recf a1 Ds1)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n len (rec Ds1)) (fun (_2 : @IRTSubsts As) => unit) (fun (_2 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => @listSortGet As i1) (Df a) Ds) => @existT (@listSortGet As i) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => @UnfoldedIRT As Ds (Df a1)) a recf) (fun (Ds : @IRTSubsts As) (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (D : @IRTDesc As) (_1 : forall (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true) -> @IRT As Ds D) (recg : forall (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true) -> let var__0   := @IRTDesc As in
+  let var__1   := @IRTSubsts As in
+  SAWCorePrelude.IRTDesc_rect As (fun (_3 : var__0) => @IRTSubsts As -> Type) (fun (i1 : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds1 (@SAWCoreScaffolding.Succ i1)) (@atIRTs As Ds1 i1)) (fun (D1 : var__0) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds1)) (fun (_3 : var__0) (recl : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @Either (recl Ds1) (recr Ds1)) (fun (_3 : var__0) (recl : @IRTSubsts As -> Type) (_4 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => prod (recl Ds1) (recr Ds1)) (fun (i1 : @SAWCoreScaffolding.Nat) (_3 : SAWCorePrelude.ListSort_rect (fun (_3 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_3 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_3 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_4 : Type) => rec n1)) As i1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As i1 -> @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @sigT (@listSortGet As i1) (fun (a : SAWCorePrelude.ListSort_rect (fun (_4 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_4 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_4 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_5 : Type) => rec n1)) As i1) => recf a Ds1)) (fun (n1 : @SAWCoreScaffolding.Nat) (len1 : @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool)) (_3 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds1 : @IRTSubsts As) => @BVVec n1 len1 (rec Ds1)) (fun (_3 : var__1) => unit) (fun (_3 : var__1) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i1 : @SAWCoreScaffolding.Nat) (_3 : @IRTSubsts As) => @listSortGet As i1) D Ds) => @genBVVec n len (@UnfoldedIRT As Ds D) recg) (fun (Ds : @IRTSubsts As) => tt) (fun (Ds : @IRTSubsts As) (i : @SAWCoreScaffolding.Nat) (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) => a).
 
 Definition foldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), forall (D : @IRTDesc As), @UnfoldedIRT As Ds D -> @IRT As Ds D :=
-  fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (D1 : @IRTDesc As) => forall (Ds1 : @IRTSubsts As), @UnfoldedIRT As Ds1 D1 -> @IRT As Ds1 D1) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds2 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds2 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n1)) Ds1 (@SAWCoreScaffolding.Succ n)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D1 : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D1 (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n1)) Ds1 n)) => @IRT_elemD As Ds1 n x) (fun (D1 : @IRTDesc As) (rec : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D1 Ds1 -> @IRT As Ds1 D1) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D2 : @IRTDesc As) (rec1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec1 (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec1 n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) D1 (@IRTs_Cons As (@IRT_mu As D1) Ds1)) => @IRT_fold As Ds1 D1 (rec (@IRTs_Cons As (@IRT_mu As D1) Ds1) x)) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : @Either (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1)) => @either (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_Either As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) => @IRT_Left As Ds1 Dl Dr (recl Ds1 xl)) (fun (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1) => @IRT_Right As Ds1 Dl Dr (recr Ds1 xr)) x) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : prod (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1)) => @uncurry (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_prod As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dl Ds1) (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n)) (@atIRTs As Ds2 n)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As n) => recf a Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n) Dr Ds1) => @IRT_pair As Ds1 Dl Dr (recl Ds1 xl) (recr Ds1 xr)) x) (fun (n : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n -> @IRTDesc As) (recf : forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n), forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds2 n1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf a1 Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds1 -> @IRT As Ds1 (Df a)) (Ds1 : @IRTSubsts As) (x : @sigT (SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds1 (Df a))) => @uncurrySigma (@listSortGet As n) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @UnfoldedIRT As Ds1 (Df a)) (@IRT As Ds1 (@IRT_sigT As n Df)) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) (xf : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (n1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ n1)) (@atIRTs As Ds2 n1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n2)) As n1 -> @IRTDesc As) (recf1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As n1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n2 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n2)) As n1) => recf1 a1 Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (n1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As n1) (Df a) Ds1) => @IRT_existT As Ds1 n Df a (recf a Ds1 xf)) x) (fun (Ds1 : @IRTSubsts As) (x : unit) => @IRT_tt As Ds1) (fun (Ds1 : @IRTSubsts As) (x : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) => @efq (@IRT As Ds1 (@IRT_empty As)) x) (fun (n : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As n) => @IRT_elemT As Ds1 n x) D Ds.
+  fun (As : @ListSort) (Ds : @IRTSubsts As) (D : @IRTDesc As) => @IRTDesc__rec As (fun (D1 : @IRTDesc As) => forall (Ds1 : @IRTSubsts As), @UnfoldedIRT As Ds1 D1 -> @IRT As Ds1 D1) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : @IRT As (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTSubsts As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRTs_Nil As) (fun (_1 : @IRTDesc As) (Ds2 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTSubsts As) => @Nat_cases (@IRTSubsts As) Ds2 (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTSubsts As) => rec n)) Ds1 (@SAWCoreScaffolding.Succ i)) (SAWCorePrelude.IRTSubsts_rect As (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.Nat -> @IRTDesc As) (fun (_1 : @SAWCoreScaffolding.Nat) => @IRT_empty As) (fun (D1 : @IRTDesc As) (_1 : @IRTSubsts As) (rec : @SAWCoreScaffolding.Nat -> @IRTDesc As) => @Nat_cases (@IRTDesc As) D1 (fun (n : @SAWCoreScaffolding.Nat) (_2 : @IRTDesc As) => rec n)) Ds1 i)) => @IRT_elemD As Ds1 i x) (fun (D1 : @IRTDesc As) (rec : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) D1 Ds1 -> @IRT As Ds1 D1) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D2 : @IRTDesc As) (rec1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec1 (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec1 n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec1 : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec1 n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec1 Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) D1 (@IRTs_Cons As (@IRT_mu As D1) Ds1)) => @IRT_fold As Ds1 D1 (rec (@IRTs_Cons As (@IRT_mu As D1) Ds1) x)) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : @Either (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1)) => @either (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_Either As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1) => @IRT_Left As Ds1 Dl Dr (recl Ds1 xl)) (fun (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1) => @IRT_Right As Ds1 Dl Dr (recr Ds1 xr)) x) (fun (Dl : @IRTDesc As) (recl : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1 -> @IRT As Ds1 Dl) (Dr : @IRTDesc As) (recr : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1 -> @IRT As Ds1 Dr) (Ds1 : @IRTSubsts As) (x : prod (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1) (SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1)) => @uncurry (@UnfoldedIRT As Ds1 Dl) (@UnfoldedIRT As Ds1 Dr) (@IRT As Ds1 (@IRT_prod As Dl Dr)) (fun (xl : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dl Ds1) (xr : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl1 Ds2) (recr1 Ds2)) (fun (_1 : @IRTDesc As) (recl1 : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr1 : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl1 Ds2) (recr1 Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i) => recf a Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) Dr Ds1) => @IRT_pair As Ds1 Dl Dr (recl Ds1 xl) (recr Ds1 xr)) x) (fun (i : @SAWCoreScaffolding.Nat) (Df : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i -> @IRTDesc As) (recf : forall (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i), forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i1)) (@atIRTs As Ds2 i1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i1 -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1) => recf a1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i1) (Df a) Ds1 -> @IRT As Ds1 (Df a)) (Ds1 : @IRTSubsts As) (x : @sigT (SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) => @UnfoldedIRT As Ds1 (Df a))) => @uncurrySigma (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) => @UnfoldedIRT As Ds1 (Df a)) (@IRT As Ds1 (@IRT_sigT As i Df)) (fun (a : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) (xf : SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i1 : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i1)) (@atIRTs As Ds2 i1)) (fun (D1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D1) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i1 -> @IRTDesc As) (recf1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1 -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i1) (fun (a1 : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n)) As i1) => recf1 a1 Ds2)) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n len (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i1 : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i1) (Df a) Ds1) => @IRT_existT As Ds1 i Df a (recf a Ds1 xf)) x) (fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (D1 : @IRTDesc As) (recg : forall (Ds1 : @IRTSubsts As), SAWCorePrelude.IRTDesc_rect As (fun (_1 : @IRTDesc As) => @IRTSubsts As -> Type) (fun (i : @SAWCoreScaffolding.Nat) (Ds2 : @IRTSubsts As) => @IRT As (@dropIRTs As Ds2 (@SAWCoreScaffolding.Succ i)) (@atIRTs As Ds2 i)) (fun (D2 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => rec (@IRTs_Cons As (@IRT_mu As D2) Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @Either (recl Ds2) (recr Ds2)) (fun (_1 : @IRTDesc As) (recl : @IRTSubsts As -> Type) (_2 : @IRTDesc As) (recr : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => prod (recl Ds2) (recr Ds2)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n1)) As i -> @IRTDesc As) (recf : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As i -> @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @sigT (@listSortGet As i) (fun (a : SAWCorePrelude.ListSort_rect (fun (_2 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_2 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_2 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n1 : @SAWCoreScaffolding.Nat) (_3 : Type) => rec n1)) As i) => recf a Ds2)) (fun (n1 : @SAWCoreScaffolding.Nat) (len1 : @SAWCoreVectorsAsCoqVectors.Vec n1 (@SAWCoreScaffolding.Bool)) (_1 : @IRTDesc As) (rec : @IRTSubsts As -> Type) (Ds2 : @IRTSubsts As) => @BVVec n1 len1 (rec Ds2)) (fun (_1 : @IRTSubsts As) => unit) (fun (_1 : @IRTSubsts As) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (i : @SAWCoreScaffolding.Nat) (_1 : @IRTSubsts As) => @listSortGet As i) D1 Ds1 -> @IRT As Ds1 D1) (Ds1 : @IRTSubsts As) (x : @BVVec n len (@UnfoldedIRT As Ds1 D1)) => @IRT_genBVVec As Ds1 n len D1 (fun (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (pf : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true)) => recg Ds1 (@atBVVec n len (@UnfoldedIRT As Ds1 D1) x i pf))) (fun (Ds1 : @IRTSubsts As) (x : unit) => @IRT_tt As Ds1) (fun (Ds1 : @IRTSubsts As) (x : @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) => @efq (@IRT As Ds1 (@IRT_empty As)) x) (fun (i : @SAWCoreScaffolding.Nat) (Ds1 : @IRTSubsts As) (x : SAWCorePrelude.ListSort_rect (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.EqP (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)) As i) => @IRT_elemT As Ds1 i x) D Ds.
 
 (* Prelude.CompM was skipped *)
 
@@ -1023,6 +1029,12 @@ Definition foldIRT : forall (As : @ListSort), forall (Ds : @IRTSubsts As), foral
 
 (* Prelude.composeM was skipped *)
 
+Definition tupleCompMFunBoth : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> prod c a -> CompM (prod c b) :=
+  fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (x : prod c a) => @bindM CompM _ b (prod c b) (f (SAWCoreScaffolding.snd x)) (fun (y : b) => @returnM CompM _ (prod c b) (pair (SAWCoreScaffolding.fst x) y)).
+
+Definition tupleCompMFunOut : forall (a : Type), forall (b : Type), forall (c : Type), c -> (a -> CompM b) -> a -> CompM (prod c b) :=
+  fun (a : Type) (b : Type) (c : Type) (x : c) (f : a -> CompM b) (y : a) => @bindM CompM _ b (prod c b) (f y) (fun (z : b) => @returnM CompM _ (prod c b) (pair x z)).
+
 (* Prelude.errorM was skipped *)
 
 (* Prelude.fixM was skipped *)
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
index b9ae5419..5322b4c4 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
@@ -1,4 +1,5 @@
 From Coq          Require Import Lists.List.
+From Coq          Require Import Logic.FunctionalExtensionality.
 Import ListNotations.
 From Coq          Require Import String.
 From Coq          Require Import Vectors.Vector.
@@ -62,10 +63,18 @@ Qed.
 
 Theorem fold_unfold_IRT As Ds D : forall x, foldIRT As Ds D (unfoldIRT As Ds D x) = x.
 Proof.
-  induction x; simpl; unfold uncurry; now f_equal.
+  induction x; simpl; unfold uncurry; f_equal; try easy.
+  (* All that remains is the IRT_BVVec case, which requires functional extensionality
+     and the fact that genBVVec and atBVVec define an isomorphism *)
+  repeat (apply functional_extensionality_dep; intro).
+  rewrite at_gen_BVVec; eauto.
 Qed.
 
 Theorem unfold_fold_IRT As Ds D : forall u, unfoldIRT As Ds D (foldIRT As Ds D u) = u.
 Proof.
-  revert Ds; induction D; try destruct u; simpl; now f_equal.
+  revert Ds; induction D; try destruct u; simpl; f_equal; try easy.
+  (* All that remains is the IRT_BVVec case, which requires functional extensionality
+     and the fact that genBVVec and atBVVec define an isomorphism *)
+  intros; rewrite <- (gen_at_BVVec _ _ _ u).
+  f_equal; repeat (apply functional_extensionality_dep; intro); eauto.
 Qed.
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index af49d3a0..46062cd7 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1607,6 +1607,11 @@ axiom at_gen_BVVec : (n : Nat) -> (len : bitvector n) -> (a : sort 0) ->
                      (ix : bitvector n) -> (pf : is_bvult n ix len) ->
                      EqP a (atBVVec n len a (genBVVec n len a f) ix pf) (f ix pf);
 
+-- Generating a BVVec by indexing another just returns the other BVVec
+axiom gen_at_BVVec : (n : Nat) -> (len : bitvector n) -> (a : sort 0) ->
+                     (x : BVVec n len a) ->
+                     EqP (BVVec n len a) (genBVVec n len a (atBVVec n len a x)) x;
+
 -- Update the value at a specific index in a BVVec
 updBVVec : (n : Nat) -> (len : bitvector n) -> (a : sort 0) ->
            BVVec n len a -> (ix : bitvector n) ->
@@ -1792,29 +1797,32 @@ foldW64List =
 -- Iso-recursive types
 
 data IRTDesc (As:ListSort) : sort 0 where {
-  IRT_varD   : Nat -> IRTDesc As; -- a IRTDesc var
+  IRT_varD   : Nat -> IRTDesc As; -- an IRTDesc var
   IRT_mu     : IRTDesc As -> IRTDesc As; -- binds a varD
   IRT_Either : IRTDesc As -> IRTDesc As -> IRTDesc As;
   IRT_prod   : IRTDesc As -> IRTDesc As -> IRTDesc As;
-  IRT_sigT   : (n:Nat) -> (listSortGet As n -> IRTDesc As) -> IRTDesc As;
+  IRT_sigT   : (i:Nat) -> (listSortGet As i -> IRTDesc As) -> IRTDesc As;
+  IRT_BVVec  : (n:Nat) -> bitvector n -> (D:IRTDesc As) -> IRTDesc As;
   IRT_unit   : IRTDesc As;
   IRT_empty  : IRTDesc As;
-  IRT_varT   : Nat -> IRTDesc As; -- a sort var, i.e. an index into `As`
+  IRT_varT   : (i:Nat) -> IRTDesc As; -- a sort var, i.e. an index into `As`
 }
 
 IRTDesc__rec : (As:ListSort) -> (P : IRTDesc As -> sort 1) ->
-               ((n:Nat) -> P (IRT_varD As n)) ->
+               ((i:Nat) -> P (IRT_varD As i)) ->
                ((D:IRTDesc As) -> P D -> P (IRT_mu As D)) ->
                ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr ->
                   P (IRT_Either As Dl Dr)) ->
                ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr ->
                   P (IRT_prod As Dl Dr)) ->
-               ((n:Nat) -> (Df : listSortGet As n -> IRTDesc As) ->
-                  ((a:listSortGet As n) -> P (Df a)) -> P (IRT_sigT As n Df)) ->
+               ((i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
+                  ((a:listSortGet As i) -> P (Df a)) -> P (IRT_sigT As i Df)) ->
+               ((n:Nat) -> (len:bitvector n) -> (D:IRTDesc As) -> P D ->
+                  P (IRT_BVVec As n len D)) ->
                P (IRT_unit As) -> P (IRT_empty As) ->
-               ((n:Nat) -> P (IRT_varT As n)) ->
+               ((i:Nat) -> P (IRT_varT As i)) ->
                (D:IRTDesc As) -> P D;
-IRTDesc__rec As P f1 f2 f3 f4 f5 f6 f7 f8 D = IRTDesc#rec As P f1 f2 f3 f4 f5 f6 f7 f8 D;
+IRTDesc__rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 D = IRTDesc#rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 D;
 
 -- A list of substitutions for a context of iso-recursive type descriptions
 data IRTSubsts (As:ListSort) : sort 0 where {
@@ -1844,29 +1852,31 @@ dropIRTs As = IRTSubsts__rec As (\ (_:IRTSubsts As) -> Nat -> IRTSubsts As)
 
 -- The type corresponding to an iso-recursive type description
 data IRT (As:ListSort) : IRTSubsts As -> IRTDesc As -> sort 0 where {
-  IRT_elemD  : (Ds:IRTSubsts As) -> (n:Nat) ->
-               IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n) ->
-               IRT As Ds (IRT_varD As n);
-  IRT_fold   : (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
-               IRT As (IRTs_Cons As (IRT_mu As D) Ds) D -> IRT As Ds (IRT_mu As D);
-  IRT_Left   : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
-               IRT As Ds Dl -> IRT As Ds (IRT_Either As Dl Dr);
-  IRT_Right  : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
-               IRT As Ds Dr -> IRT As Ds (IRT_Either As Dl Dr);
-  IRT_pair   : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
-               IRT As Ds Dl -> IRT As Ds Dr -> IRT As Ds (IRT_prod As Dl Dr);
-  IRT_existT : (Ds:IRTSubsts As) -> (n:Nat) -> (Df : listSortGet As n -> IRTDesc As) ->
-               (a:listSortGet As n) -> IRT As Ds (Df a) -> IRT As Ds (IRT_sigT As n Df);
-  IRT_tt     : (Ds:IRTSubsts As) -> IRT As Ds (IRT_unit As);
-  IRT_elemT  : (Ds:IRTSubsts As) -> (n:Nat) ->
-               listSortGet As n -> IRT As Ds (IRT_varT As n);
+  IRT_elemD    : (Ds:IRTSubsts As) -> (i:Nat) ->
+                 IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i) ->
+                 IRT As Ds (IRT_varD As i);
+  IRT_fold     : (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
+                 IRT As (IRTs_Cons As (IRT_mu As D) Ds) D -> IRT As Ds (IRT_mu As D);
+  IRT_Left     : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
+                 IRT As Ds Dl -> IRT As Ds (IRT_Either As Dl Dr);
+  IRT_Right    : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
+                 IRT As Ds Dr -> IRT As Ds (IRT_Either As Dl Dr);
+  IRT_pair     : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
+                 IRT As Ds Dl -> IRT As Ds Dr -> IRT As Ds (IRT_prod As Dl Dr);
+  IRT_existT   : (Ds:IRTSubsts As) -> (i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
+                 (a:listSortGet As i) -> IRT As Ds (Df a) -> IRT As Ds (IRT_sigT As i Df);
+  IRT_genBVVec : (Ds:IRTSubsts As) -> (n:Nat) -> (len:bitvector n) -> (D:IRTDesc As) ->
+                 ((i:bitvector n) -> is_bvult n i len -> IRT As Ds D) -> IRT As Ds (IRT_BVVec As n len D);
+  IRT_tt       : (Ds:IRTSubsts As) -> IRT As Ds (IRT_unit As);
+  IRT_elemT    : (Ds:IRTSubsts As) -> (i:Nat) ->
+                 listSortGet As i -> IRT As Ds (IRT_varT As i);
 }
 
 IRT__rec : (As:ListSort) -> (P : (Ds:IRTSubsts As) -> (D:IRTDesc As) -> IRT As Ds D -> sort 1) ->
-           ((Ds:IRTSubsts As) -> (n:Nat) ->
-              (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) ->
-              P (dropIRTs As Ds (Succ n)) (atIRTs As Ds n) x ->
-              P Ds (IRT_varD As n) (IRT_elemD As Ds n x)) ->
+           ((Ds:IRTSubsts As) -> (i:Nat) ->
+              (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) ->
+              P (dropIRTs As Ds (Succ i)) (atIRTs As Ds i) x ->
+              P Ds (IRT_varD As i) (IRT_elemD As Ds i x)) ->
            ((Ds:IRTSubsts As) -> (D:IRTDesc As) ->
               (x:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D) ->
               P (IRTs_Cons As (IRT_mu As D) Ds) D x ->
@@ -1879,20 +1889,24 @@ IRT__rec : (As:ListSort) -> (P : (Ds:IRTSubsts As) -> (D:IRTDesc As) -> IRT As D
               (xl:IRT As Ds Dl) -> P Ds Dl xl ->
               (xr:IRT As Ds Dr) -> P Ds Dr xr ->
               P Ds (IRT_prod As Dl Dr) (IRT_pair As Ds Dl Dr xl xr)) ->
-           ((Ds:IRTSubsts As) -> (n:Nat) -> (Df : listSortGet As n -> IRTDesc As) ->
-              (a:listSortGet As n) -> (xf:IRT As Ds (Df a)) -> P Ds (Df a) xf ->
-              P Ds (IRT_sigT As n Df) (IRT_existT As Ds n Df a xf)) ->
+           ((Ds:IRTSubsts As) -> (i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
+              (a:listSortGet As i) -> (xf:IRT As Ds (Df a)) -> P Ds (Df a) xf ->
+              P Ds (IRT_sigT As i Df) (IRT_existT As Ds i Df a xf)) ->
+           ((Ds:IRTSubsts As) -> (n:Nat) -> (len:bitvector n) -> (D:IRTDesc As) ->
+              (xg : (i:bitvector n) -> is_bvult n i len -> IRT As Ds D) ->
+              ((i:bitvector n) -> (pf:is_bvult n i len) -> P Ds D (xg i pf)) ->
+              P Ds (IRT_BVVec As n len D) (IRT_genBVVec As Ds n len D xg)) ->
            ((Ds:IRTSubsts As) -> P Ds (IRT_unit As) (IRT_tt As Ds)) ->
-           ((Ds:IRTSubsts As) -> (n:Nat) -> (a:listSortGet As n) ->
-              P Ds (IRT_varT As n) (IRT_elemT As Ds n a)) ->
+           ((Ds:IRTSubsts As) -> (i:Nat) -> (a:listSortGet As i) ->
+              P Ds (IRT_varT As i) (IRT_elemT As Ds i a)) ->
            (Ds:IRTSubsts As) -> (D:IRTDesc As) -> (x:IRT As Ds D) -> P Ds D x;
-IRT__rec As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x = IRT#rec As P f1 f2 f3 f4 f5 f6 f7 f8 Ds D x;
+IRT__rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 Ds D x = IRT#rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 Ds D x;
 
 -- The type of a once-unfolded iso-recursive type
 UnfoldedIRT : (As:ListSort) -> IRTSubsts As -> IRTDesc As -> sort 0;
 UnfoldedIRT As Ds D = IRTDesc__rec As (\ (_:IRTDesc As) -> IRTSubsts As -> sort 0)
-  (\ (n:Nat) (Ds:IRTSubsts As) ->
-      IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n))
+  (\ (i:Nat) (Ds:IRTSubsts As) ->
+      IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i))
   (\ (D:IRTDesc As) (rec : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
       rec (IRTs_Cons As (IRT_mu As D) Ds))
   (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0)
@@ -1901,20 +1915,23 @@ UnfoldedIRT As Ds D = IRTDesc__rec As (\ (_:IRTDesc As) -> IRTSubsts As -> sort
   (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0)
      (_:IRTDesc As) (recr : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
       recl Ds * recr Ds)
-  (\ (n:Nat) (_ : listSortGet As n -> IRTDesc As)
-     (recf : listSortGet As n -> IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
-      Sigma (listSortGet As n) (\ (a:listSortGet As n) -> recf a Ds))
+  (\ (i:Nat) (_ : listSortGet As i -> IRTDesc As)
+     (recf : listSortGet As i -> IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
+      Sigma (listSortGet As i) (\ (a:listSortGet As i) -> recf a Ds))
+  (\ (n:Nat) (len:bitvector n) (_:IRTDesc As)
+     (rec : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
+      BVVec n len (rec Ds))
   (\ (_:IRTSubsts As) -> #())
   (\ (_:IRTSubsts As) -> EqP Bool True False)
-  (\ (n:Nat) (_:IRTSubsts As) -> listSortGet As n) D Ds;
+  (\ (i:Nat) (_:IRTSubsts As) -> listSortGet As i) D Ds;
 
 -- `fold` and `unfold` for IRTs
 
 unfoldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
             IRT As Ds D -> UnfoldedIRT As Ds D;
 unfoldIRT As = IRT__rec As (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As Ds D) -> UnfoldedIRT As Ds D)
-  (\ (Ds:IRTSubsts As) (n:Nat) (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n))
-     (_:UnfoldedIRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) -> x)
+  (\ (Ds:IRTSubsts As) (i:Nat) (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i))
+     (_:UnfoldedIRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) -> x)
   (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D)
      (rec: UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) -> rec)
   (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As)
@@ -1927,17 +1944,21 @@ unfoldIRT As = IRT__rec As (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As Ds D) -
      (_:IRT As Ds Dl) (recl:UnfoldedIRT As Ds Dl)
      (_:IRT As Ds Dr) (recr:UnfoldedIRT As Ds Dr) ->
       (recl, recr))
-  (\ (Ds:IRTSubsts As) (n:Nat) (Df : listSortGet As n -> IRTDesc As) (a:listSortGet As n)
+  (\ (Ds:IRTSubsts As) (i:Nat) (Df : listSortGet As i -> IRTDesc As) (a:listSortGet As i)
      (_:IRT As Ds (Df a)) (recf:UnfoldedIRT As Ds (Df a)) ->
-      exists (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a)) a recf)
+      exists (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a)) a recf)
+  (\ (Ds:IRTSubsts As) (n:Nat) (len:bitvector n) (D:IRTDesc As)
+     (_ : (i:bitvector n) -> is_bvult n i len -> IRT As Ds D)
+     (recg : (i:bitvector n) -> is_bvult n i len -> UnfoldedIRT As Ds D) ->
+      genBVVec n len (UnfoldedIRT As Ds D) recg)
   (\ (Ds:IRTSubsts As) -> ())
-  (\ (Ds:IRTSubsts As) (n:Nat) (a:listSortGet As n) -> a);
+  (\ (Ds:IRTSubsts As) (i:Nat) (a:listSortGet As i) -> a);
 
 foldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
           UnfoldedIRT As Ds D -> IRT As Ds D;
 foldIRT As Ds D = IRTDesc__rec As (\ (D:IRTDesc As) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
-  (\ (n:Nat) (Ds:IRTSubsts As) (x:IRT As (dropIRTs As Ds (Succ n)) (atIRTs As Ds n)) ->
-      IRT_elemD As Ds n x)
+  (\ (i:Nat) (Ds:IRTSubsts As) (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) ->
+      IRT_elemD As Ds i x)
   (\ (D:IRTDesc As) (rec : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
      (Ds:IRTSubsts As) (x:UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) ->
       IRT_fold As Ds D (rec (IRTs_Cons As (IRT_mu As D) Ds) x))
@@ -1953,15 +1974,19 @@ foldIRT As Ds D = IRTDesc__rec As (\ (D:IRTDesc As) -> (Ds:IRTSubsts As) -> Unfo
       uncurry (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) (IRT As Ds (IRT_prod As Dl Dr))
               (\ (xl:UnfoldedIRT As Ds Dl) (xr:UnfoldedIRT As Ds Dr) ->
                   IRT_pair As Ds Dl Dr (recl Ds xl) (recr Ds xr)) x)
-  (\ (n:Nat) (Df : listSortGet As n -> IRTDesc As)
-     (recf : (a:listSortGet As n) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds (Df a) -> IRT As Ds (Df a))
-     (Ds:IRTSubsts As) (x:Sigma (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a))) ->
-      uncurrySigma (listSortGet As n) (\ (a:listSortGet As n) -> UnfoldedIRT As Ds (Df a)) (IRT As Ds (IRT_sigT As n Df))
-                   (\ (a:listSortGet As n) (xf:UnfoldedIRT As Ds (Df a)) ->
-                       IRT_existT As Ds n Df a (recf a Ds xf)) x)
+  (\ (i:Nat) (Df : listSortGet As i -> IRTDesc As)
+     (recf : (a:listSortGet As i) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds (Df a) -> IRT As Ds (Df a))
+     (Ds:IRTSubsts As) (x:Sigma (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a))) ->
+      uncurrySigma (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a)) (IRT As Ds (IRT_sigT As i Df))
+                   (\ (a:listSortGet As i) (xf:UnfoldedIRT As Ds (Df a)) ->
+                       IRT_existT As Ds i Df a (recf a Ds xf)) x)
+  (\ (n:Nat) (len:bitvector n) (D:IRTDesc As) (recg : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
+     (Ds:IRTSubsts As) (x : BVVec n len (UnfoldedIRT As Ds D)) ->
+      IRT_genBVVec As Ds n len D (\ (i:bitvector n) (pf:is_bvult n i len) ->
+                                     recg Ds (atBVVec n len (UnfoldedIRT As Ds D) x i pf)))
   (\ (Ds:IRTSubsts As) (x:#()) -> IRT_tt As Ds)
   (\ (Ds:IRTSubsts As) (x:EqP Bool True False) -> efq (IRT As Ds (IRT_empty As)) x)
-  (\ (n:Nat) (Ds:IRTSubsts As) (x:listSortGet As n) -> IRT_elemT As Ds n x) D Ds;
+  (\ (i:Nat) (Ds:IRTSubsts As) (x:listSortGet As i) -> IRT_elemT As Ds i x) D Ds;
 
 
 --------------------------------------------------------------------------------