let rec mk_inj i x = if i <= 0 then mk_inl x else if i = 1 then mk_inr x else mk_inr (mk_inj (i - 1) x)