IndProp

[clayrat]

Feels like I'm stuck at filter_not_empty_In' here. First I construct Reflect using beq_natP {n} {m=x}, but when I try to match on it (either via case or with), I get (assuming the false case first):

Type mismatch between
        Reflect (n = x) False (Type of ReflectF notp)
and
        Reflect (n = x) (beq_nat n x) (Expected type)

[clayrat]

Ok, I think I've figured out the Reflect thing - it seems to work if you define it as

data Reflect : (p : Type) -> (b : Bool) -> Type where
  ReflectT : p -> (b=True) -> Reflect p b
  ReflectF : (Not p) -> (b=False) -> Reflect p b

[clayrat]

Ready for review

[yurrriq]

Thanks! I'll take a look today.

[yurrriq]

This is looking pretty good. I'm gonna merge it now and then PR some edits for you.