blob: 2423b77b550c1573c0b960d21258ea49ac8f47d4 (
plain)
1
2
3
4
|
The command has indeed failed with message:
Tactic failure: Goal is solvable by congruence but some arguments are missing.
Try "congruence with ((Triple a _ _)) ((Triple d c _))",
replacing metavariables by arbitrary terms.
|
