proposition: Lemma DropName_Cons_Some_neq : forall `{FacadeWrapper (Value av) A} k k' v (tail: A -> Telescope av), k <> k' -> (DropName k (Cons (NTSome k') v tail)) = (Cons (NTSome k') v (fun vv => DropName k (tail vv))).
proof: Proof. intros; simpl. destruct (string_dec _ _); (congruence || reflexivity). Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas