proposition: Lemma CompileWhileFalse_Loop: forall {av} (vtest : StringMap.key) (env : GLabelMap.t (FuncSpec av)) (ext : StringMap.t (Value av)) (tenv : Telescope av) tenv' body, TelEq ext tenv tenv' -> vtest ∉ ext -> NotInTelescope vtest tenv -> {{[[`vtest ->> (Word.natToWord 32 1) as _]]::tenv }} (DFacade.While (TestE IL.Eq vtest O) body) {{ tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros * H **. rewrite <- H. apply CompileDeallocW_discretely; eauto. apply CompileWhileFalse. reflexivity. unfold Lifted_is_false, LiftPropertyToTelescope, is_true, is_false, eval_bool, eval; repeat match goal with | _ => SameValues_Facade_t_step | _ => facade_cleanup_call | _ => progress simpl end. Qed.
imports: CertifiedExtraction.Extraction.DeallocSCA CertifiedExtraction.Extraction.External.Core