lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →
lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n →
loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) →