At:
fappend-inject n,m:, f:((n-1)(m-1)). Inj((n-1); (m-1); f) Inj(n; m; f[n-1:=m-1])
By:
Auto
THEN
ParallelOp -1
THEN
RepeatFor 2 (Analyze 0)
THEN
Unfold `fappend` 0
THEN
Reduce 0
THEN
RepeatFor 2 SplitOnConclITE
THEN
BackThruSomeHyp
Generated subgoals:
n,m:
, f:(
Inj(