proposition: Lemma isisolatedinstn { n : nat } ( x : ⟦n⟧ ) : isisolated _ x.
proof: Proof. intros. apply ( isisolatedinclb ( stntonat n ) ( isinclstntonat n ) x ( isisolatedn x ) ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions