diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 37d0099..99e499d 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -62,7 +62,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | _ => SSet.empty
 
 /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
-def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do
+def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
   let recursorType ← Meta.inferType recursor
   let resultant ← mvarId.getType
@@ -95,11 +95,11 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.Inductio
   mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
   newMVars := newMVars ++ [goalConduit]
 
-  return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!})
+  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
 
 def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   let recursor ← Elab.Term.elabTerm (stx := stx) .none
   let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
-  Elab.Tactic.setGoals $ nextGoals.map (·.mvarId)
+  Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
 
 end Pantograph.Tactic
diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean
index c67102c..58c6050 100644
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@@ -24,8 +24,8 @@ def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
 
 structure BranchResult where
   fvarId?: Option FVarId := .none
-  main: MVarId
   branch: MVarId
+  main: MVarId
 
 def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
   mvarId.checkNotAssigned `Pantograph.Tactic.have
@@ -47,8 +47,8 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
 
   return {
     fvarId? := .some fvarId,
-    main := mvarUpstream.mvarId!,
     branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
   }
 
 def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
@@ -74,8 +74,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
     pure mvarUpstream
 
   return {
-    main := mvarUpstream.mvarId!,
     branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
   }
 
 def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do