fact: Fixpoint gen_init_state_aux (s : seq nat) (p : pos) (st : state) {struct s} : option state := if s is a :: s1 then let p1 := next p in if (a \in sref) then if in_state p a st then let st1 := rm_state p st in gen_init_state_aux s1 p1 (update_anti_literals p a st1) else None else gen_init_state_aux s1 p1 st else some st.
imports: mathcomp(all_ssreflect) mathcomp(zify)