by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
conclude
(min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
- = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
- = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
+ = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
+ = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH222(*END*).
(*END*)
done.
case FOr.
by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
conclude
(max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
- = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
- = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
+ = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
+ = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH222.
(*END*)
done.
case FImpl.