proposition: Lemma DropName_Cons_None : forall `{FacadeWrapper (Value av) A} k v (tail: A -> Telescope av), (DropName k (Cons NTNone v tail)) = (Cons NTNone v (fun vv => DropName k (tail vv))).
proof: Proof. intros; simpl; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas