proposition: Lemma Idr_SET : Idr_law Comp_SET Id_SET.
proof: Proof. unfold Idr_law in |- *; intros. unfold Comp in |- *. unfold Ap2 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. intro x; apply Refl. Qed.
imports: Category