Library Nijn.TerminationTechniques.NonTermination.NonTerminationTactics
Require Import List.
Ltac solve_In :=
cbn -[
In] ;
match goal with
| [ |-
In ?
x (?
x :: _) ] ⇒
left ;
reflexivity
| [ |-
In ?
x (?
y :: _) ] ⇒
right ;
solve_In
| [ |-
In _ nil ] ⇒
fail
end.