Output argument of f1 is list. But f1 depends on f2.
match f1 (c :: f2 k (c' :: l3)) with |  => false | [r0] => true | r0 :: (_ :: _) as l5 =>
To simplify above ,what step i should take?
1) induction (f1 (c :: f2 k (c' :: l3)))
2) unfold f2.
3) match l5 with =true (meaning of this statement? c exist and c' does not exist or under what condition l5 is nil and it is true?
Last updated: Oct 04 2023 at 23:01 UTC