PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: reg g wf

V,T:Type, G:Grammar(V;T). RegG(G) Prop
By:
Unfold `reg_g` 0
THEN
Analyze
THEN
Inst Thm* a:A, as:A*. ||a.as|| = ||as||+1 [V+T;inl(A);nil]
THEN
RWH (HypC 8) 0
THEN
RWH (LemmaC Thm* ||nil|| = 0) 0
Generated subgoals:

None

About:
alluniversememberproplistequalint
consaddnatural_numberunioninlnil