None

Conclusion:

x.rec_ind(x;f,x1.case x1: x (y.case y: x4 case ext{decidable__equal_Var} x x4 of inl(l) => inl Ax | inr(r) => inr (z.any (r Ax)) ; x4 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); y6y7 (inr (z.Ax) );); x (y.case y: x1 (inr (z.Ax) ); x1 case f x x1 of inl(l) => inl Ax | inr(r) => inr (z.any (r Ax)) ; x2x3 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); y2y3 (inr (z.Ax) );); x1x2 (y.case y: x (inr (x.Ax) ); x (inr (z.Ax) ); x3x4 case f x1 x3 of inl(l) => case f x2 x4 of inl(l1) => inl Ax | inr(r) => inr (z.any (r Ax)) | inr(r) => inr (z.any (r Ax)) ; x3x4 (inr (%3.Ax) ); y2y3 (inr (%3.Ax) );); x1x2 (y.case y: x (inr (z.Ax) ); x (inr (z.Ax) ); x3x4 (inr (z.Ax) ); x3x4 case f x1 x3 of inl(l) => case f x2 x4 of inl(l1) => inl Ax | inr(r) => inr (z.any (r Ax)) | inr(r) => inr (z.any (r Ax)) ; y2y3 (inr (z.Ax) );); y2y3 (y.case y: x (inr (z.Ax) ); x (inr (z.Ax) ); x1x2 (inr (z.Ax) ); x1x2 (inr (z.Ax) ); y5y6 case f y2 y5 of inl(l) => case f y3 y6 of inl(l1) => inl Ax | inr(r) => inr (z.any (r Ax)) | inr(r) => inr (z.any (r Ax)) ;);)

None