proposition: Lemma restrict_single i: restrict _ _ (tsingle i) ≡ ttsingle i.
proof: Proof. intros [a|a j [b|???]]; simpl; try lattice. split. now intros [_ H]. intros <-. repeat constructor. Qed.
imports: prop monoid positives comparisons