proposition: Lemma di_eq1 {i x} : x < i → di i x = x.
proof: Proof. intros lt. unfold di. induction (natlthorgeh x i) as [_|P]. - apply idpath. - apply fromempty. exact (natgehtonegnatlth _ _ P lt). Defined.
imports: UniMath.Foundations.Sets