At: reach lemma 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. nn: 
5. f: nn
Alph
6. g: Alphnn
7. Fin(S.car)
8. InvFuns(nn; Alph; f; g)
[si] 
{y:{x:(S.car*)| 0 < ||x|| & ||x||
0+1 }| y[(||y||-1)] = si }
By:
Analyze THENL [Analyze;Reduce 0;Analyze -1]
THEN
Reduce 0
Generated subgoals:None
About:
