lemma sem_uni_step :
accGRealize ? uni_step us_acc Pre_uni_step
R_uni_step_true R_uni_step_false.
+@daemon (* this no longer works: TODO *) (*
@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false))
? (test_char_inv …) (sem_nop …) …)
[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???)
#b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' %
// cases b in Hb'; normalize #H1 //
]
+*)
qed.
(*