proposition: Lemma TelEq_TelAppend_Cons_Second {av A B}: forall {H : FacadeWrapper (Value av) B} (t1: Telescope av) t2 k (v : Comp A) ext, TelEq ext ([[ k ~~> v as vv]] :: TelAppend t1 (t2 vv)) (TelAppend t1 ([[ k ~~> v as vv]] :: (t2 vv))).
proof: Proof. intros. induction t1; simpl. + reflexivity. + rewrite TelEq_swap. setoid_rewrite H0. reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedPropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas