- (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) =
- min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)).
- by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11).
- by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22).
- by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111).
- by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
+ (min ([[ F1[ G1/x ] ]]v) ([[ F2[ G1/x ] ]]v) =
+ min ([[ F1[ G2/x ] ]]v) ([[ F2[ G2/x ] ]]v)).
+ by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]v1 = [[ F1[ G2/x ] ]]v1) (IH11).
+ by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]v2 = [[ F2[ G2/x ] ]]v2) (IH22).
+ by IH11 we proved ([[ F1[ G1/x ] ]]v = [[ F1[ G2/x ] ]]v) (IH111).
+ by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]v = [[ F2[ G2/x ] ]]v) (IH222).