The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 12/04/2010 07:28, Jianzhou Zhao a écrit :
> But (a1, a1') seems a subtern of (A2 a1, A2 a1')
> to me, because a1 and a1' are subterms of
> A2 a1 and A2 a1' respectively.
>
> Thanks
>    


If you  consider the terms   written without the usual  notation: i.e.
(pair (A2 a1) (A2 a1')) and (pair a1 a1') ,  you notice that the second 
one is not a subtree of the first one (because of the A2's between the 
root and the terms a1 and a1' )

Pierre