blob: 5cfb8f1ff4c67739c9fa3cb5254e50ef4a32da45 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Inductive list A := Node : node A -> list A
with node A := Nil | Cons : A -> list A -> node A.
Fixpoint app {A} (l1 l2 : list A) {struct l1} : list A
with app_node {A} (n1 : node A) (l2 : list A) {struct n1} : node A.
Proof.
+ destruct l1 as [n]; constructor.
exact (app_node _ n l2).
+ destruct n1 as [|x l1].
- destruct l2 as [n2]; exact n2.
- exact (Cons _ x (app _ l1 l2)).
Qed.
|
