proposition: Lemma TelEq_swap: forall {av A A' ext} (k: @NameTag av A) (k': @NameTag av A') (v: Comp A) (v': Comp A') (tenv: A -> A' -> Telescope av), TelEq ext ([[k ~~> v as vv]] :: [[k' ~~> v' as vv']] :: tenv vv vv') ([[k' ~~> v' as vv']] :: [[k ~~> v as vv]] :: tenv vv vv').
proof: Proof. destruct k, k'; unfold TelEq; repeat match goal with | _ => SameValues_Facade_t_step | _ => progress SameValues_Fiat_t_step | [ H: StringMap.MapsTo _ _ (StringMap.remove _ _) |- _ ] => learn (remove_mapsto H) | _ => rewrite remove_remove_comm; congruence end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas