Assume H1: TransSet {tagn}.

We prove the intermediate claim L1: 0 ∈ {tagn}.

Apply H1 tagn (SingI tagn) to the current goal.

We will prove 0 ∈ tagn.

An exact proof term for the current goal is nat_trans tagn tagn_nat 1 tagn_1 0 In_0_1.

Apply In_no2cycle 0 1 In_0_1 to the current goal.

We will prove 1 ∈ 0.

rewrite the current goal using SingE tagn 0 L1 (from left to right) at position 2.

We will prove 1 ∈ tagn.

An exact proof term for the current goal is tagn_1.

∎