proposition: Lemma TelEq_chomp_head_heterogeneous : forall {av A B} {WA: FacadeWrapper (Value av) A} {WB: FacadeWrapper (Value av) B} k (a: A) (b: B) (tenv tenv': Telescope av) ext, wrap a = wrap b -> TelEq ext tenv tenv' -> TelEq ext ([[ ` k ->> a as _]] :: tenv) ([[ ` k ->> b as _]] :: tenv).
proof: Proof. intros. unfold TelEq; SameValues_Fiat_t. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core