proposition: Lemma SameValues_TelStrongEq_1 : forall {A} ext (tenv1 tenv2 : Telescope A) st, TelStrongEq tenv1 tenv2 -> (st ≲ tenv1 ∪ ext <-> st ≲ tenv2 ∪ ext).
proof: Proof. induction tenv1; destruct tenv2; repeat match goal with | _ => cleanup | _ => TelStrongEq_t | [ H: Monad.equiv ?a _, H': context[?a] |- _ ] => rewrite H in H' | _ => SameValues_Fiat_t end. rewrite <- H; eauto. rewrite <- H; eauto. rewrite -> H; eauto. rewrite -> H; eauto. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas