在我的另一个问题之后，我尝试使用 Idris for实现类型驱动开发same_cons中的实际练习，以证明给定两个相等的列表，将相同的元素添加到每个列表会导致两个相等的列表。
例子：
prove that 1 :: [1,2,3] == 1 :: [1,2,3]
所以我想出了以下编译代码：
sameS : {xs : List a} -> {ys : List a} -> (x: a) -> xs = ys -> x :: xs = x :: ys
sameS {xs} {ys} x prf = cong prf
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons prf = sameS _ prf
我可以通过以下方式调用它：
> same_cons {x=5} {xs = [1,2,3]} {ys = [1,2,3]} Refl
Refl : [5, 1, 2, 3] = [5, 1, 2, 3]
关于cong函数，我的理解是它需要一个证明，即a = b，但我不明白它的第二个参数：f a.
> :t cong
cong : (a = b) -> f a = f b
请解释。