proposition: Lemma restrict_inj n p: restrict n n (tinj p) ≡ ttinj n p.
proof: Proof. intros [b|b i w]; simpl. 2: simpl; lattice. split. now intros [_ H]. intros ?. split. constructor. assumption. Qed.
imports: prop monoid positives comparisons