{A B:Type0 } (va:Vars A) (vb:Vars B) : Vars (sum@{Set Set} A B) := fun i => match i with inl i => va i | inr i => vb i end. Section Lookup. Class Lookup {A:Type0 } (x: R) (f: Vars A) := { lookup: A; lookup_correct: f lookup = x }. Global Arguments lookup {A} x f {_}. Context (x:R) {A B:Type0 } (va : Vars A) (vb : Vars B). Local Instance lookup_l `{!Lookup x va} : Lookup x ( va vb). Proof. exists (inl (lookup x va)). apply lookup_correct. Defined.
Require Import