interpretation
"functional non-negative application (total relocation maps)"
'ApplySucc f l = (tr_nap f l).
lemma tr_nap_unfold (f) (l):
interpretation
"functional non-negative application (total relocation maps)"
'ApplySucc f l = (tr_nap f l).
lemma tr_nap_unfold (f) (l):