typeside t schema s1 : t schema s2 : t mapping m : s1 -> s2 instance i : s1 ---------------------------------- instance (sigma_chase m i ) : s2