proposition: Lemma SameValues_Cons_unfold_None : forall {av A} (st: State av) (val: Comp A) ext tail, st ≲ (Cons NTNone val tail) ∪ ext -> exists v, val ↝ v /\ st ≲ tail v ∪ ext.
proof: Proof. simpl; intros; assumption. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas