proposition: Lemma Lifted_is_true_eq_MapsTo : forall {av} ext tenv var (v: W), Lifted_MapsTo (av := av) ext tenv var (wrap v) -> Lifted_is_true ext tenv (var = v)%facade.
proof: Proof. unfold Lifted_is_true, Lifted_MapsTo, LiftPropertyToTelescope, is_true, is_false, eval_bool, eval. repeat match goal with | _ => cleanup_facade_pure | _ => SameValues_Facade_t_step | [ H: forall _, _ -> _, H': _ |- _ ] => specialize (H _ H') | _ => progress simpl end. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas